Definition df-f1 5501

Description: Define a one-to-one function. For equivalent definitions see dff12 5688 and dff13 6067. 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 5493	. 2 wff F : A -1-1-> B
5	1, 2, 3	wf 5492	. . 3 wff F : A --> B
6	3	ccnv 4912	. . . 4 class `' F
7	6	wfun 5490	. . 3 wff Fun `' F
8	5, 7	wa 367	. 2 wff ( F : A --> B /\ Fun `' F )
9	4, 8	wb 184	1 wff ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )

This definition is referenced by:  f1eq1  5684  f1eq2  5685  f1eq3  5686  nff1  5687  dff12  5688  f1f  5689  f1ss  5694  f1ssr  5695  f1ssres  5696  f1cnvcnv  5697  f1co  5698  dff1o2  5729  f1f1orn  5735  f1imacnv  5740  f10  5755  nvof1o  6087  fun11iun  6659  f11o  6661  f1o2ndf1  6807  tz7.48lem  7024  ssdomg  7480  domunsncan  7536  sbthlem9  7554  fodomr  7587  1sdom  7639  fsuppcolem  7775  fsuppco  7776  enfin1ai  8677  injresinj  11825  isercolllem2  13490  isercoll  13492  ismon2  15140  isepi2  15147  isfth2  15321  fthoppc  15329  odf1o2  16710  frlmlbs  18917  f1lindf  18942  istrl2  24661  wlkntrllem3  24684  spthonepeq  24710  wlkdvspthlem  24730  wlkdvspth  24731  usgra2wlkspthlem1  24740  usgra2wlkspthlem2  24741  cyclnspth  24752  constr3trllem2  24772  4cycl4dv  24788  usg2wotspth  25005  2spontn0vne  25008  eupatrl  25089  rinvf1o  27610  omssubadd  28427  subfacp1lem3  28815  subfacp1lem5  28817  diophrw  30857  usgra2pthspth  32669  spthdifv  32670  usgra2pth  32672