Definition df-f1 5549

Description: Define a one-to-one function. For equivalent definitions see dff12 5738 and dff13 6118. 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 5541	. 2 wff F : A -1-1-> B
5	1, 2, 3	wf 5540	. . 3 wff F : A --> B
6	3	ccnv 4795	. . . 4 class `' F
7	6	wfun 5538	. . 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  5734  f1eq2  5735  f1eq3  5736  nff1  5737  dff12  5738  f1f  5739  f1ss  5744  f1ssr  5745  f1ssres  5746  f1cnvcnv  5747  f1co  5748  dff1o2  5779  f1f1orn  5785  f1imacnv  5790  f10  5805  nvof1o  6138  fun11iun  6711  f11o  6713  f1o2ndf1  6859  tz7.48lem  7113  ssdomg  7569  domunsncan  7625  sbthlem9  7643  fodomr  7676  1sdom  7728  fsuppcolem  7867  fsuppco  7868  enfin1ai  8765  injresinj  11975  isercolllem2  13672  isercoll  13674  ismon2  15582  isepi2  15589  isfth2  15763  fthoppc  15771  odf1o2  17165  frlmlbs  19297  f1lindf  19322  istrl2  25210  wlkntrllem3  25233  spthonepeq  25259  wlkdvspthlem  25279  wlkdvspth  25280  usgra2wlkspthlem1  25289  usgra2wlkspthlem2  25290  cyclnspth  25301  constr3trllem2  25321  4cycl4dv  25337  usg2wotspth  25554  2spontn0vne  25557  eupatrl  25638  rinvf1o  28176  madjusmdetlem4  28608  omssubadd  29080  omssubaddOLD  29084  subfacp1lem3  29857  subfacp1lem5  29859  diophrw  35513  subusgr  39108  usgra2pthspth  39266  spthdifv  39267  usgra2pth  39269