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

Definition df-f1 4825
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 (𝐹:A1-1B ↔ (𝐹:AB Fun 𝐹))

Detailed syntax breakdown of Definition df-f1
StepHypRef Expression
1 cA . . 3 class A
2 cB . . 3 class B
3 cF . . 3 class 𝐹
41, 2, 3wf1 4817 . 2 wff 𝐹:A1-1B
51, 2, 3wf 4816 . . 3 wff 𝐹:AB
63ccnv 4262 . . . 4 class 𝐹
76wfun 4814 . . 3 wff Fun 𝐹
85, 7wa 97 . 2 wff (𝐹:AB Fun 𝐹)
94, 8wb 98 1 wff (𝐹:A1-1B ↔ (𝐹:AB Fun 𝐹))
Colors of variables: wff set class
This definition is referenced by:  f1eq1  5003  f1eq2  5004  f1eq3  5005  nff1  5006  dff12  5007  f1f  5008  f1ss  5013  f1ssr  5014  f1ssres  5015  f1cnvcnv  5016  f1co  5017  dff1o2  5047  f1f1orn  5053  f1imacnv  5059  fun11iun  5063  f11o  5075  f10  5076  f1o2ndf1  5763
  Copyright terms: Public domain W3C validator