Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-f1 GIF version

Definition df-f1 5128
 Description: Define a one-to-one function. Compare Definition 6.15(5) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow). (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
df-f1 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))

Detailed syntax breakdown of Definition df-f1
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
3 cF . . 3 class 𝐹
41, 2, 3wf1 5120 . 2 wff 𝐹:𝐴1-1𝐵
51, 2, 3wf 5119 . . 3 wff 𝐹:𝐴𝐵
63ccnv 4538 . . . 4 class 𝐹
76wfun 5117 . . 3 wff Fun 𝐹
85, 7wa 103 . 2 wff (𝐹:𝐴𝐵 ∧ Fun 𝐹)
94, 8wb 104 1 wff (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))
 Colors of variables: wff set class This definition is referenced by:  f1eq1  5323  f1eq2  5324  f1eq3  5325  nff1  5326  dff12  5327  f1f  5328  f1ss  5334  f1ssr  5335  f1ssres  5337  f1cnvcnv  5339  f1co  5340  dff1o2  5372  f1f1orn  5378  f1imacnv  5384  fun11iun  5388  f11o  5400  f10  5401  f1o2ndf1  6125  ssdomg  6672  phplem4dom  6756  sbthlemi9  6853  casefun  6970  casef1  6975  djufun  6989  exmidfodomrlemim  7057  ennnfonelemf1  11931
 Copyright terms: Public domain W3C validator