Theorem f1oeq3 5627

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 5596	. . 3 |- ( A = B -> ( F : C -1-1-> A <-> F : C -1-1-> B ) )
2		foeq3 5611	. . 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 5418	. 2 |- ( F : C -1-1-onto-> A <-> ( F : C -1-1-> A /\ F : C -onto-> A ) )
5		df-f1o 5418	. 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 5408   -onto->wfo 5409   -1-1-onto->wf1o 5410

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 2418

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2424  df-cleq 2430  df-clel 2433  df-in 3328  df-ss 3335  df-f 5415  df-f1 5416  df-fo 5417  df-f1o 5418

This theorem is referenced by:  f1oeq23  5628  f1oeq123d  5631  f1ores  5648  resdif  5654  resin  5655  f1osng  5672  f1oresrab  5868  fveqf1o  5993  isoeq5  6007  isoini2  6023  ncanth  6043  oacomf1o  6996  mapsnf1o  7296  bren  7311  xpcomf1o  7392  domss2  7462  isinf  7518  wemapwe  7920  wemapweOLD  7921  oef1o  7922  oef1oOLD  7923  cnfcomlem  7924  cnfcom2  7927  cnfcom3  7929  cnfcom3clem  7930  cnfcomlemOLD  7932  cnfcom2OLD  7935  cnfcom3OLD  7937  cnfcom3clemOLD  7938  infxpenc  8176  infxpenc2lem1  8177  infxpenc2  8180  infxpencOLD  8181  infxpenc2OLD  8184  ackbij2lem2  8401  fin1a2lem6  8566  hsmexlem1  8587  pwfseqlem5  8822  pwfseq  8823  hashgf1o  11785  axdc4uzlem  11796  sumeq1  13158  fsumss  13194  fsumcnv  13232  unbenlem  13961  4sqlem11  14008  pwssnf1o  14428  catcisolem  14966  yoniso  15087  xpsmnd  15453  gsumvalx  15493  gsumpropd  15495  xpsgrp  15663  cayley  15908  cayleyth  15909  gsumval3OLD  16371  gsumval3lem1  16372  gsumval3lem2  16373  gsumcom2  16453  coe1mul2lem2  17693  cncfcnvcn  20466  ovolicc2lem4  20972  logf1o2  22064  iseupa  23531  adjbd1o  25434  rinvf1o  25894  gsumpropd2lem  26189  eulerpartgbij  26703  eulerpartlemgh  26709  derangval  27003  subfacp1lem2a  27016  subfacp1lem3  27018  subfacp1lem5  27020  elgiso  27262  prodeq1f  27368  fprodss  27408  fprodcnv  27441  ismtyval  28642  ismrer1  28680  rngoisoval  28726  pwfi2f1o  29394  imasgim  29398  clwwlkvbij  30406  bj-finsumval0  32337  lautset  33477  pautsetN  33493  hvmap1o2  35161