NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-f1o GIF version

Definition df-f1o 4794
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 5291, dff1o3 5292, dff1o4 5294, and dff1o5 5295. Compare Definition 6.15(6) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow and "onto" below the arrow). (Contributed by SF, 5-Jan-2015.)
Assertion
Ref Expression
df-f1o (F:A1-1-ontoB ↔ (F:A1-1B F:AontoB))

Detailed syntax breakdown of Definition df-f1o
StepHypRef Expression
1 cA . . 3 class A
2 cB . . 3 class B
3 cF . . 3 class F
41, 2, 3wf1o 4780 . 2 wff F:A1-1-ontoB
51, 2, 3wf1 4778 . . 3 wff F:A1-1B
61, 2, 3wfo 4779 . . 3 wff F:AontoB
75, 6wa 358 . 2 wff (F:A1-1B F:AontoB)
84, 7wb 176 1 wff (F:A1-1-ontoB ↔ (F:A1-1B F:AontoB))
Colors of variables: wff setvar class
This definition is referenced by:  f1oeq1  5281  f1oeq2  5282  f1oeq3  5283  nff1o  5285  f1of1  5286  dff1o2  5291  dff1o5  5295  f1oco  5308  fo00  5318  f1o0  5319  dff1o6  5475
  Copyright terms: Public domain W3C validator