Theorem dff1o4 5591

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 5588	. 2 |- ( F : A -1-1-onto-> B <-> ( F Fn A /\ Fun `' F /\ ran F = B ) )
2		3anass 1008	. 2 |- ( ( F Fn A /\ Fun `' F /\ ran F = B ) <-> ( F Fn A /\ ( Fun `' F /\ ran F = B ) ) )
3		df-rn 4736	. . . . . 6 |- ran F = dom `' F
4	3	eqeq1i 2239	. . . . 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 5329	. . . 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 1004   = wceq 1397   `'ccnv 4724   dom cdm 4725   ran crn 4726   Fun wfun 5320   Fn wfn 5321   -1-1-onto->wf1o 5325

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213  df-rn 4736  df-fn 5329  df-f 5330  df-f1 5331  df-fo 5332  df-f1o 5333

This theorem is referenced by:  f1ocnv  5596  f1oun  5603  f1o00  5620  f1oi  5623  f1osn  5625  f1ompt  5798  f1ofveu  6005  f1ocnvd  6224  f1od2  6399  mapsnf1o2  6864  sbthlemi9  7163  xnn0nnen  10698  nninfctlemfo  12610  mhmf1o  13552  grpinvf1o  13652  ghmf1o  13861  rhmf1o  14181  hmeof1o2  15031