Theorem f1oeq2 5813

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

Assertion

Ref	Expression
f1oeq2

Proof of Theorem f1oeq2

Step	Hyp	Ref	Expression
1		f1eq2 5782	. . 3
2		foeq2 5797	. . 3
3	1, 2	anbi12d 710	. 2
4		df-f1o 5600	. 2
5		df-f1o 5600	. 2
6	3, 4, 5	3bitr4g 288	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  -1-1->wf1 5590  -onto->wfo 5591  -1-1-onto->wf1o 5592

This theorem is referenced by:  f1oeq23  5815  f1oeq123d  5818  resin  5842  f1osng  5859  f1o2sn  6074  fveqf1o  6205  isoeq4  6218  oacomf1o  7233  bren  7545  marypha1lem  7913  oef1o  8162  oef1oOLD  8163  cnfcomlem  8164  cnfcom  8165  cnfcom2  8167  cnfcomlemOLD  8172  cnfcomOLD  8173  cnfcom2OLD  8175  infxpenc  8416  infxpenc2  8420  infxpencOLD  8421  infxpenc2OLD  8424  pwfseqlem5  9062  pwfseq  9063  summolem3  13536  summo  13539  fsum  13542  fsumf1o  13545  sumsn  13563  prodmolem3  13740  prodmo  13743  fprod  13748  fprodf1o  13753  prodsn  13767  gsumvalx  15897  gsumpropd  15899  gsumpropd2lem  15900  gsumval3OLD  16908  gsumval3lem1  16909  gsumval3  16911  znhash  18597  znunithash  18603  imasf1oxms  20992  cncfcnvcn  21425  wlknwwlknvbij  24740  clwwlkvbij  24801  eupai  24967  eupatrl  24968  eupa0  24974  eupares  24975  eupap1  24976  derangval  28611  subfacp1lem2a  28624  subfacp1lem3  28626  subfacp1lem5  28628  erdsze2lem1  28647  elgiso  29036  ismtyval  30296  rngoisoval  30380  eldioph2lem1  30693  imasgim  31048  sumsnd  31401  sumsnf  31570  prodsnf  31587  stoweidlem35  31817  stoweidlem39  31821  f1dmvrnfibi  32312  lautset  35806  pautsetN  35822

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2449  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600