Theorem f1oeq2 5623

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 5589	. . 3 |- ( A = B -> ( F : A -1-1-> C <-> F : B -1-1-> C ) )
2		foeq2 5607	. . 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 5379	. 2 |- ( F : A -1-1-onto-> C <-> ( F : A -1-1-> C /\ F : A -onto-> C ) )
5		df-f1o 5379	. 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 1402   -1-1->wf1 5369   -onto->wfo 5370   -1-1-onto->wf1o 5371

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-fn 5375  df-f 5376  df-f1 5377  df-fo 5378  df-f1o 5379

This theorem is referenced by:  f1oeq23  5625  f1oeq123d  5628  f1oeq2d  5630  f1osng  5677  isoeq4  6000  breng  7019  bren  7020  f1dmvrnfibi  7248  summodclem3  12125  summodclem2a  12126  summodc  12128  fsum3  12132  fsumf1o  12135  sumsnf  12154  fprodf1o  12333  prodsnf  12337  znfi  14962  znhash  14963