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

Definition df-f1 4931
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 4923 . 2 wff 𝐹:𝐴1-1𝐵
51, 2, 3wf 4922 . . 3 wff 𝐹:𝐴𝐵
63ccnv 4364 . . . 4 class 𝐹
76wfun 4920 . . 3 wff Fun 𝐹
85, 7wa 102 . 2 wff (𝐹:𝐴𝐵 ∧ Fun 𝐹)
94, 8wb 103 1 wff (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))
Colors of variables: wff set class
This definition is referenced by:  f1eq1  5112  f1eq2  5113  f1eq3  5114  nff1  5115  dff12  5116  f1f  5117  f1ss  5122  f1ssr  5123  f1ssres  5124  f1cnvcnv  5125  f1co  5126  dff1o2  5156  f1f1orn  5162  f1imacnv  5168  fun11iun  5172  f11o  5184  f10  5185  f1o2ndf1  5874  ssdomg  6317  phplem4dom  6387
  Copyright terms: Public domain W3C validator