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  12163  summodclem2a  12164  summodc  12166  fsum3  12170  fsumf1o  12173  sumsnf  12192  fprodf1o  12371  prodsnf  12375  znfi  15039  znhash  15040