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

Definition df-f1 4792
Description: Define a one-to-one function. For equivalent definitions see dff12 5257 and dff13 5471. Compare Definition 6.15(5) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow). (Contributed by SF, 5-Jan-2015.)
Assertion
Ref Expression
df-f1 (F:A1-1B ↔ (F:A–→B Fun F))

Detailed syntax breakdown of Definition df-f1
StepHypRef Expression
1 cA . . 3 class A
2 cB . . 3 class B
3 cF . . 3 class F
41, 2, 3wf1 4778 . 2 wff F:A1-1B
51, 2, 3wf 4777 . . 3 wff F:A–→B
63ccnv 4771 . . . 4 class F
76wfun 4775 . . 3 wff Fun F
85, 7wa 358 . 2 wff (F:A–→B Fun F)
94, 8wb 176 1 wff (F:A1-1B ↔ (F:A–→B Fun F))
Colors of variables: wff setvar class
This definition is referenced by:  f1eq1  5253  f1eq2  5254  f1eq3  5255  nff1  5256  dff12  5257  f1f  5258  f1ss  5262  f1funfun  5263  f1co  5264  dff1o2  5291  f1f1orn  5297  f1ores  5300  f1imacnv  5302  fun11iun  5305  f11o  5315  f10  5316  enpw1  6062  ncdisjun  6136  sbthlem1  6203
  Copyright terms: Public domain W3C validator