Definition df-f1 5583

Description: Define a one-to-one function. For equivalent definitions see dff12 5770 and dff13 6151. 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 5575	. 2 wff F : A -1-1-> B
5	1, 2, 3	wf 5574	. . 3 wff F : A --> B
6	3	ccnv 4988	. . . 4 class `' F
7	6	wfun 5572	. . 3 wff Fun `' F
8	5, 7	wa 369	. 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  5766  f1eq2  5767  f1eq3  5768  nff1  5769  dff12  5770  f1f  5771  f1ss  5776  f1ssr  5777  f1ssres  5778  f1cnvcnv  5779  f1co  5780  dff1o2  5811  f1f1orn  5817  f1imacnv  5822  f10  5837  nvof1o  6171  fun11iun  6745  f11o  6747  f1o2ndf1  6893  tz7.48lem  7108  ssdomg  7563  domunsncan  7619  sbthlem9  7637  fodomr  7670  1sdom  7724  fsuppcolem  7862  fsuppco  7863  enfin1ai  8767  injresinj  11908  isercolllem2  13470  isercoll  13472  ismon2  15111  isepi2  15118  isfth2  15263  fthoppc  15271  odf1o2  16572  frlmlbs  18809  f1lindf  18835  istrl2  24518  wlkntrllem3  24541  spthonepeq  24567  wlkdvspthlem  24587  wlkdvspth  24588  usgra2wlkspthlem1  24597  usgra2wlkspthlem2  24598  cyclnspth  24609  constr3trllem2  24629  4cycl4dv  24645  usg2wotspth  24862  2spontn0vne  24865  eupatrl  24946  rinvf1o  27450  subfacp1lem3  28604  subfacp1lem5  28606  diophrw  30668  usgra2pthspth  32305  spthdifv  32306  usgra2pth  32308