Description: Extend the definition of a wff to include one-to-one onto functions. (Read: F maps A one-to-one onto B .) The notation ("1-1" above the arrow and "onto" below the arrow) is from Definition 6.15(6) of TakeutiZaring p. 27.
| Ref | Expression | ||
|---|---|---|---|
| Assertion | wf1o | wff 𝐹 : 𝐴 –1-1-onto→ 𝐵 |