Theorem f1oeq2 5581

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 5547	. . 3 |- ( A = B -> ( F : A -1-1-> C <-> F : B -1-1-> C ) )
2		foeq2 5565	. . 3 |- ( A = B -> ( F : A -onto-> C <-> F : B -onto-> C ) )
3	1, 2	anbi12d 473	. 2 |- ( A = B -> ( ( F : A -1-1-> C /\ F : A -onto-> C ) <-> ( F : B -1-1-> C /\ F : B -onto-> C ) ) )
4		df-f1o 5340	. 2 |- ( F : A -1-1-onto-> C <-> ( F : A -1-1-> C /\ F : A -onto-> C ) )
5		df-f1o 5340	. 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 ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1398   -1-1->wf1 5330   -onto->wfo 5331   -1-1-onto->wf1o 5332

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-fn 5336  df-f 5337  df-f1 5338  df-fo 5339  df-f1o 5340

This theorem is referenced by:  f1oeq23  5583  f1oeq123d  5586  f1oeq2d  5588  f1osng  5635  isoeq4  5955  breng  6959  bren  6960  f1dmvrnfibi  7186  summodclem3  12021  summodclem2a  12022  summodc  12024  fsum3  12028  fsumf1o  12031  sumsnf  12050  fprodf1o  12229  prodsnf  12233  znfi  14751  znhash  14752