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

Definition df-f1 5054
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 5046 . 2 wff 𝐹:𝐴1-1𝐵
51, 2, 3wf 5045 . . 3 wff 𝐹:𝐴𝐵
63ccnv 4466 . . . 4 class 𝐹
76wfun 5043 . . 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  5246  f1eq2  5247  f1eq3  5248  nff1  5249  dff12  5250  f1f  5251  f1ss  5257  f1ssr  5258  f1ssres  5260  f1cnvcnv  5262  f1co  5263  dff1o2  5293  f1f1orn  5299  f1imacnv  5305  fun11iun  5309  f11o  5321  f10  5322  f1o2ndf1  6031  ssdomg  6575  phplem4dom  6658  sbthlemi9  6754  casefun  6856  casef1  6861  djufun  6866  exmidfodomrlemim  6924
  Copyright terms: Public domain W3C validator