Definition df-f1 5418

Description: Define a one-to-one function. For equivalent definitions see dff12 5597 and dff13 5963. 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 5410	. 2 wff F : A -1-1-> B
5	1, 2, 3	wf 5409	. . 3 wff F : A --> B
6	3	ccnv 4836	. . . 4 class `' F
7	6	wfun 5407	. . 3 wff Fun `' F
8	5, 7	wa 359	. 2 wff ( F : A --> B /\ Fun `' F )
9	4, 8	wb 177	1 wff ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )

This definition is referenced by:  f1eq1  5593  f1eq2  5594  f1eq3  5595  nff1  5596  dff12  5597  f1f  5598  f1ss  5603  f1ssr  5604  f1ssres  5605  f1cnvcnv  5606  f1co  5607  dff1o2  5638  f1f1orn  5644  f1imacnv  5650  fun11iun  5654  f11o  5667  f10  5668  f1o2ndf1  6413  tz7.48lem  6657  abianfp  6675  ssdomg  7112  domunsncan  7167  sbthlem9  7184  fodomr  7217  1sdom  7270  suppfif1  7358  enfin1ai  8220  injresinj  11155  isercolllem2  12414  isercoll  12416  ismon2  13915  isepi2  13922  isfth2  14067  fthoppc  14075  odf1o2  15162  istrl2  21491  wlkntrllem3  21514  spthonepeq  21540  wlkdvspthlem  21560  wlkdvspth  21561  cyclnspth  21571  constr3trllem2  21591  4cycl4dv  21607  eupatrl  21643  nvof1o  23993  rinvf1o  23995  subfacp1lem3  24821  subfacp1lem5  24823  diophrw  26707  frlmlbs  27117  f1lindf  27160  usgra2pthspth  28035  usgra2wlkspthlem1  28036  usgra2wlkspthlem2  28037  spthdifv  28039  usgra2pth  28041  usg2wotspth  28081  2spontn0vne  28084