Theorem f1oeq3 5451

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 5418	. . 3 |- ( A = B -> ( F : C -1-1-> A <-> F : C -1-1-> B ) )
2		foeq3 5436	. . 3 |- ( A = B -> ( F : C -onto-> A <-> F : C -onto-> B ) )
3	1, 2	anbi12d 473	. 2 |- ( A = B -> ( ( F : C -1-1-> A /\ F : C -onto-> A ) <-> ( F : C -1-1-> B /\ F : C -onto-> B ) ) )
4		df-f1o 5223	. 2 |- ( F : C -1-1-onto-> A <-> ( F : C -1-1-> A /\ F : C -onto-> A ) )
5		df-f1o 5223	. 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 ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1353   -1-1->wf1 5213   -onto->wfo 5214   -1-1-onto->wf1o 5215

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3135  df-ss 3142  df-f 5220  df-f1 5221  df-fo 5222  df-f1o 5223

This theorem is referenced by:  f1oeq23  5452  f1oeq123d  5455  f1oeq3d  5458  f1ores  5476  resdif  5483  f1osng  5502  f1oresrab  5681  isoeq5  5805  isoini2  5819  mapsnf1o  6736  bren  6746  xpcomf1o  6824  frechashgf1o  10427  sumeq1  11362  fisumss  11399  fsumcnv  11444  prodeq1f  11559  ennnfonelemhf1o  12413  ennnfonelemex  12414  ssnnctlemct  12446