Definition df-f1o 5551

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 5779, dff1o3 5780, dff1o4 5782, and dff1o5 5783. Compare Definition 6.15(6) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow and "onto" below the arrow). (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
df-f1o	|- ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )

Detailed syntax breakdown of Definition df-f1o

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3		cF	. . 3 class F
4	1, 2, 3	wf1o 5543	. 2 wff F : A -1-1-onto-> B
5	1, 2, 3	wf1 5541	. . 3 wff F : A -1-1-> B
6	1, 2, 3	wfo 5542	. . 3 wff F : A -onto-> B
7	5, 6	wa 370	. 2 wff ( F : A -1-1-> B /\ F : A -onto-> B )
8	4, 7	wb 187	1 wff ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )

This definition is referenced by:  f1oeq1  5765  f1oeq2  5766  f1oeq3  5767  nff1o  5772  f1of1  5773  dff1o2  5779  dff1o5  5783  f1oco  5796  fo00  5808  dff1o6  6133  nvof1o  6138  fcof1od  6151  soisoi  6178  f1oweALT  6735  tposf1o2  6954  smoiso2  7043  f1finf1o  7751  unfilem2  7789  fofinf1o  7805  alephiso  8480  cnref1o  11248  wwlktovf1o  12978  1arith  14814  xpsff1o  15417  isffth2  15764  ffthf1o  15767  orbsta  16910  symgextf1o  17007  symgfixf1o  17024  odf1o1  17164  znf1o  19064  cygznlem3  19082  scmatf1o  19499  m2cpmf1o  19723  pm2mpf1o  19781  reeff1o  23344  recosf1o  23426  efif1olem4  23436  dvdsmulf1o  24065  wlknwwlknbij  25383  wlkiswwlkbij  25390  wwlkextbij0  25402  clwwlkf1o  25468  clwlkf1oclwwlk  25521  eupatrl  25638  frgrancvvdeqlem8  25710  numclwlk1lem2f1o  25766  unopf1o  27511  ghomf1olem  30264  poimirlem26  31873  poimirlem27  31874  wessf1ornlem  37363  projf1o  37378  sumnnodd  37593  dvnprodlem1  37704  fourierdlem54  37907