Theorem f1oeq3 5632

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

Assertion

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

Proof of Theorem f1oeq3

Step	Hyp	Ref	Expression
1		f1eq3 5598	. . 3 |- ( A = B -> ( F : C -1-1-> A <-> F : C -1-1-> B ) )
2		foeq3 5616	. . 3 |- ( A = B -> ( F : C -onto-> A <-> F : C -onto-> B ) )
3	1, 2	anbi12d 477	. 2 |- ( A = B -> ( ( F : C -1-1-> A /\ F : C -onto-> A ) <-> ( F : C -1-1-> B /\ F : C -onto-> B ) ) )
4		df-f1o 5387	. 2 |- ( F : C -1-1-onto-> A <-> ( F : C -1-1-> A /\ F : C -onto-> A ) )
5		df-f1o 5387	. 2 |- ( F : C -1-1-onto-> B <-> ( F : C -1-1-> B /\ F : C -onto-> B ) )
6	3, 4, 5	3bitr4g 223	1 |- ( A = B -> ( F : C -1-1-onto-> A <-> F : C -1-1-onto-> B ) )

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

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-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233  df-f 5384  df-f1 5385  df-fo 5386  df-f1o 5387

This theorem is used by:  f1oeq23  5633  f1oeq123d  5636  f1oeq3d  5639  f1ores  5657  resdif  5664  f1osng  5685  f1oresrab  5876  isoeq5  6014  isoini2  6028  rinvf1o  6038  mapsnf1o  7023  breng  7033  bren  7034  xpcomf1o  7127  frechashgf1o  10886  sumeq1  12146  fisumss  12184  fsumcnv  12229  prodeq1f  12344  4sqlem11  13209  ennnfonelemhf1o  13362  ennnfonelemex  13363  ssnnctlemct  13395  uspgredgiedg  16624