Definition df-f1 5606

Description: Define a one-to-one function. For equivalent definitions see dff12 5801 and dff13 6184. 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 4852	. . . 4 class `' F
7	6	wfun 5595	. . 3 wff Fun `' F
8	5, 7	wa 375	. 2 wff ( F : A --> B /\ Fun `' F )
9	4, 8	wb 189	1 wff ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )

This definition is referenced by:  f1eq1  5797  f1eq2  5798  f1eq3  5799  nff1  5800  dff12  5801  f1f  5802  f1ss  5807  f1ssr  5808  f1ssres  5809  f1cnvcnv  5810  f1co  5811  dff1o2  5842  f1f1orn  5848  f1imacnv  5853  f10  5868  nvof1o  6204  fun11iun  6780  f11o  6782  f1o2ndf1  6931  tz7.48lem  7184  ssdomg  7641  domunsncan  7698  sbthlem9  7716  fodomr  7749  1sdom  7801  fsuppcolem  7940  fsuppco  7941  enfin1ai  8840  injresinj  12057  isercolllem2  13778  isercoll  13780  ismon2  15688  isepi2  15695  isfth2  15869  fthoppc  15877  odf1o2  17271  frlmlbs  19404  f1lindf  19429  istrl2  25317  wlkntrllem3  25340  spthonepeq  25366  wlkdvspthlem  25386  wlkdvspth  25387  usgra2wlkspthlem1  25396  usgra2wlkspthlem2  25397  cyclnspth  25408  constr3trllem2  25428  4cycl4dv  25444  usg2wotspth  25661  2spontn0vne  25664  eupatrl  25745  rinvf1o  28279  madjusmdetlem4  28705  omssubadd  29177  omssubaddOLD  29181  subfacp1lem3  29954  subfacp1lem5  29956  diophrw  35646  fpropnf1  39078  subusgr  39411  usgrislfuspgr  39720  upgrf1istrl  39738  pthdivtx  39762  spthdep  39766  upgrwlkdvdelem  39768  upgrwlkdvde  39769  spthonepeq-av  39784  pthdlem1  39792  uspgrn2crct  39826  usgra2pthspth  39938  spthdifv  39939  usgra2pth  39941