Theorem f1oeq3 5655

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 5624	. . 3 |- ( A = B -> ( F : C -1-1-> A <-> F : C -1-1-> B ) )
2		foeq3 5639	. . 3 |- ( A = B -> ( F : C -onto-> A <-> F : C -onto-> B ) )
3	1, 2	anbi12d 710	. 2 |- ( A = B -> ( ( F : C -1-1-> A /\ F : C -onto-> A ) <-> ( F : C -1-1-> B /\ F : C -onto-> B ) ) )
4		df-f1o 5446	. 2 |- ( F : C -1-1-onto-> A <-> ( F : C -1-1-> A /\ F : C -onto-> A ) )
5		df-f1o 5446	. 2 |- ( F : C -1-1-onto-> B <-> ( F : C -1-1-> B /\ F : C -onto-> B ) )
6	3, 4, 5	3bitr4g 288	1 |- ( A = B -> ( F : C -1-1-onto-> A <-> F : C -1-1-onto-> B ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1369   -1-1->wf1 5436   -onto->wfo 5437   -1-1-onto->wf1o 5438

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-in 3356  df-ss 3363  df-f 5443  df-f1 5444  df-fo 5445  df-f1o 5446

This theorem is referenced by:  f1oeq23  5656  f1oeq123d  5659  f1ores  5676  resdif  5682  resin  5683  f1osng  5700  f1oresrab  5896  fveqf1o  6021  isoeq5  6035  isoini2  6051  ncanth  6071  oacomf1o  7025  mapsnf1o  7325  bren  7340  xpcomf1o  7421  domss2  7491  isinf  7547  wemapwe  7949  wemapweOLD  7950  oef1o  7951  oef1oOLD  7952  cnfcomlem  7953  cnfcom2  7956  cnfcom3  7958  cnfcom3clem  7959  cnfcomlemOLD  7961  cnfcom2OLD  7964  cnfcom3OLD  7966  cnfcom3clemOLD  7967  infxpenc  8205  infxpenc2lem1  8206  infxpenc2  8209  infxpencOLD  8210  infxpenc2OLD  8213  ackbij2lem2  8430  fin1a2lem6  8595  hsmexlem1  8616  pwfseqlem5  8851  pwfseq  8852  hashgf1o  11814  axdc4uzlem  11825  sumeq1  13187  fsumss  13223  fsumcnv  13261  unbenlem  13990  4sqlem11  14037  pwssnf1o  14457  catcisolem  14995  yoniso  15116  xpsmnd  15482  gsumvalx  15523  gsumpropd  15525  gsumpropd2lem  15526  xpsgrp  15695  cayley  15940  cayleyth  15941  gsumval3OLD  16403  gsumval3lem1  16404  gsumval3lem2  16405  gsumcom2  16489  coe1mul2lem2  17744  cncfcnvcn  20519  ovolicc2lem4  21025  logf1o2  22117  iseupa  23608  adjbd1o  25511  rinvf1o  25971  eulerpartgbij  26777  eulerpartlemgh  26783  derangval  27077  subfacp1lem2a  27090  subfacp1lem3  27092  subfacp1lem5  27094  elgiso  27337  prodeq1f  27443  fprodss  27483  fprodcnv  27516  ismtyval  28725  ismrer1  28763  rngoisoval  28809  pwfi2f1o  29477  imasgim  29481  clwwlkvbij  30489  mat2cnstpmatrngiso  31105  bj-finsumval0  32679  lautset  33822  pautsetN  33838  hvmap1o2  35506