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

Definition df-f1 4834
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 4826 . 2 wff 𝐹:A1-1B
51, 2, 3wf 4825 . . 3 wff 𝐹:AB
63ccnv 4271 . . . 4 class 𝐹
76wfun 4823 . . 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  5012  f1eq2  5013  f1eq3  5014  nff1  5015  dff12  5016  f1f  5017  f1ss  5022  f1ssr  5023  f1ssres  5024  f1cnvcnv  5025  f1co  5026  dff1o2  5056  f1f1orn  5062  f1imacnv  5068  fun11iun  5072  f11o  5084  f10  5085  f1o2ndf1  5772
  Copyright terms: Public domain W3C validator