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

Definition df-f1 4850
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 4842 . 2 wff 𝐹:A1-1B
51, 2, 3wf 4841 . . 3 wff 𝐹:AB
63ccnv 4287 . . . 4 class 𝐹
76wfun 4839 . . 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  5030  f1eq2  5031  f1eq3  5032  nff1  5033  dff12  5034  f1f  5035  f1ss  5040  f1ssr  5041  f1ssres  5042  f1cnvcnv  5043  f1co  5044  dff1o2  5074  f1f1orn  5080  f1imacnv  5086  fun11iun  5090  f11o  5102  f10  5103  f1o2ndf1  5791  ssdomg  6194
  Copyright terms: Public domain W3C validator