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

Definition df-f1 5188
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 5180 . 2 wff 𝐹:𝐴1-1𝐵
51, 2, 3wf 5179 . . 3 wff 𝐹:𝐴𝐵
63ccnv 4598 . . . 4 class 𝐹
76wfun 5177 . . 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  5383  f1eq2  5384  f1eq3  5385  nff1  5386  dff12  5387  f1f  5388  f1ss  5394  f1ssr  5395  f1ssres  5397  f1cnvcnv  5399  f1co  5400  dff1o2  5432  f1f1orn  5438  f1imacnv  5444  fun11iun  5448  f11o  5460  f10  5461  f1o2ndf1  6188  ssdomg  6736  phplem4dom  6820  sbthlemi9  6922  casefun  7042  casef1  7047  djufun  7061  exmidfodomrlemim  7149  ennnfonelemf1  12305
  Copyright terms: Public domain W3C validator