Theorem dff1o4 5529

Description: Alternate definition of one-to-one onto function. (Contributed by NM, 25-Mar-1998.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)

Assertion

Ref	Expression
dff1o4	|- ( F : A -1-1-onto-> B <-> ( F Fn A /\ `' F Fn B ) )

Proof of Theorem dff1o4

Step	Hyp	Ref	Expression
1		dff1o2 5526	. 2 |- ( F : A -1-1-onto-> B <-> ( F Fn A /\ Fun `' F /\ ran F = B ) )
2		3anass 984	. 2 |- ( ( F Fn A /\ Fun `' F /\ ran F = B ) <-> ( F Fn A /\ ( Fun `' F /\ ran F = B ) ) )
3		df-rn 4685	. . . . . 6 |- ran F = dom `' F
4	3	eqeq1i 2212	. . . . 5 |- ( ran F = B <-> dom `' F = B )
5	4	anbi2i 457	. . . 4 |- ( ( Fun `' F /\ ran F = B ) <-> ( Fun `' F /\ dom `' F = B ) )
6		df-fn 5273	. . . 4 |- ( `' F Fn B <-> ( Fun `' F /\ dom `' F = B ) )
7	5, 6	bitr4i 187	. . 3 |- ( ( Fun `' F /\ ran F = B ) <-> `' F Fn B )
8	7	anbi2i 457	. 2 |- ( ( F Fn A /\ ( Fun `' F /\ ran F = B ) ) <-> ( F Fn A /\ `' F Fn B ) )
9	1, 2, 8	3bitri 206	1 |- ( F : A -1-1-onto-> B <-> ( F Fn A /\ `' F Fn B ) )

Syntax hints:   /\ wa 104   <-> wb 105   /\ w3a 980   = wceq 1372   `'ccnv 4673   dom cdm 4674   ran crn 4675   Fun wfun 5264   Fn wfn 5265   -1-1-onto->wf1o 5269

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-11 1528  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-3an 982  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-in 3171  df-ss 3178  df-rn 4685  df-fn 5273  df-f 5274  df-f1 5275  df-fo 5276  df-f1o 5277

This theorem is referenced by:  f1ocnv  5534  f1oun  5541  f1o00  5556  f1oi  5559  f1osn  5561  f1ompt  5730  f1ofveu  5931  f1ocnvd  6147  f1od2  6320  mapsnf1o2  6782  sbthlemi9  7066  xnn0nnen  10580  nninfctlemfo  12332  mhmf1o  13273  grpinvf1o  13373  ghmf1o  13582  rhmf1o  13901  hmeof1o2  14751