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

Definition df-f1 5098
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 5090 . 2 wff 𝐹:𝐴1-1𝐵
51, 2, 3wf 5089 . . 3 wff 𝐹:𝐴𝐵
63ccnv 4508 . . . 4 class 𝐹
76wfun 5087 . . 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  5293  f1eq2  5294  f1eq3  5295  nff1  5296  dff12  5297  f1f  5298  f1ss  5304  f1ssr  5305  f1ssres  5307  f1cnvcnv  5309  f1co  5310  dff1o2  5340  f1f1orn  5346  f1imacnv  5352  fun11iun  5356  f11o  5368  f10  5369  f1o2ndf1  6093  ssdomg  6640  phplem4dom  6724  sbthlemi9  6821  casefun  6938  casef1  6943  djufun  6957  exmidfodomrlemim  7025  ennnfonelemf1  11842
  Copyright terms: Public domain W3C validator