Definition df-f1 5606

Description: Define a one-to-one function. For equivalent definitions see dff12 5795 and dff13 6174. 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	|- ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )

Detailed syntax breakdown of Definition df-f1

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3		cF	. . 3 class F
4	1, 2, 3	wf1 5598	. 2 wff F : A -1-1-> B
5	1, 2, 3	wf 5597	. . 3 wff F : A --> B
6	3	ccnv 4853	. . . 4 class `' F
7	6	wfun 5595	. . 3 wff Fun `' F
8	5, 7	wa 370	. 2 wff ( F : A --> B /\ Fun `' F )
9	4, 8	wb 187	1 wff ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )

This definition is referenced by:  f1eq1  5791  f1eq2  5792  f1eq3  5793  nff1  5794  dff12  5795  f1f  5796  f1ss  5801  f1ssr  5802  f1ssres  5803  f1cnvcnv  5804  f1co  5805  dff1o2  5836  f1f1orn  5842  f1imacnv  5847  f10  5862  nvof1o  6194  fun11iun  6767  f11o  6769  f1o2ndf1  6915  tz7.48lem  7166  ssdomg  7622  domunsncan  7678  sbthlem9  7696  fodomr  7729  1sdom  7781  fsuppcolem  7920  fsuppco  7921  enfin1ai  8812  injresinj  12022  isercolllem2  13707  isercoll  13709  ismon2  15590  isepi2  15597  isfth2  15771  fthoppc  15779  odf1o2  17160  frlmlbs  19286  f1lindf  19311  istrl2  25113  wlkntrllem3  25136  spthonepeq  25162  wlkdvspthlem  25182  wlkdvspth  25183  usgra2wlkspthlem1  25192  usgra2wlkspthlem2  25193  cyclnspth  25204  constr3trllem2  25224  4cycl4dv  25240  usg2wotspth  25457  2spontn0vne  25460  eupatrl  25541  rinvf1o  28070  madjusmdetlem4  28495  omssubadd  28961  subfacp1lem3  29693  subfacp1lem5  29695  diophrw  35310  usgra2pthspth  38421  spthdifv  38422  usgra2pth  38424