Theorem f1oeq2 5628

Description: Equality theorem for one-to-one onto functions. (Contributed by NM, 10-Feb-1997.)

Assertion

Ref	Expression
f1oeq2	|- ( A = B -> ( F : A -1-1-onto-> C <-> F : B -1-1-onto-> C ) )

Proof of Theorem f1oeq2

Step	Hyp	Ref	Expression
1		f1eq2 5594	. . 3 |- ( A = B -> ( F : A -1-1-> C <-> F : B -1-1-> C ) )
2		foeq2 5612	. . 3 |- ( A = B -> ( F : A -onto-> C <-> F : B -onto-> C ) )
3	1, 2	anbi12d 477	. 2 |- ( A = B -> ( ( F : A -1-1-> C /\ F : A -onto-> C ) <-> ( F : B -1-1-> C /\ F : B -onto-> C ) ) )
4		df-f1o 5384	. 2 |- ( F : A -1-1-onto-> C <-> ( F : A -1-1-> C /\ F : A -onto-> C ) )
5		df-f1o 5384	. 2 |- ( F : B -1-1-onto-> C <-> ( F : B -1-1-> C /\ F : B -onto-> C ) )
6	3, 4, 5	3bitr4g 223	1 |- ( A = B -> ( F : A -1-1-onto-> C <-> F : B -1-1-onto-> C ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1402   -1-1->wf1 5374   -onto->wfo 5375   -1-1-onto->wf1o 5376

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-fn 5380  df-f 5381  df-f1 5382  df-fo 5383  df-f1o 5384

This theorem is used by:  f1oeq23  5630  f1oeq123d  5633  f1oeq2d  5635  f1osng  5682  isoeq4  6010  breng  7029  bren  7030  f1dmvrnfibi  7258  summodclem3  12147  summodclem2a  12148  summodc  12150  fsum3  12154  fsumf1o  12157  sumsnf  12176  fprodf1o  12355  prodsnf  12359  znfi  14990  znhash  14991