Theorem f1oeq1 5812

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

Assertion

Ref	Expression
f1oeq1

Proof of Theorem f1oeq1

Step	Hyp	Ref	Expression
1		f1eq1 5781	. . 3
2		foeq1 5796	. . 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:  f1oeq123d  5818  f1ocnvb  5834  f1orescnv  5836  resin  5842  f1ovi  5857  f1osng  5859  f1oresrab  6063  fsn  6069  fveqf1o  6205  isoeq1  6215  f1oexbi  6750  oacomf1o  7233  mapsn  7480  mapsnf1o3  7487  f1oen3g  7551  ensn1  7599  xpcomf1o  7626  omf1o  7640  enfixsn  7646  domss2  7696  php3  7723  isinf  7753  ssfi  7760  oef1o  8162  oef1oOLD  8163  cnfcomlem  8164  cnfcom  8165  cnfcom2  8167  cnfcom3  8169  cnfcom3clem  8170  cnfcomlemOLD  8172  cnfcomOLD  8173  cnfcom2OLD  8175  cnfcom3OLD  8177  cnfcom3clemOLD  8178  infxpenc  8416  infxpenc2lem2  8418  infxpenc2  8420  infxpencOLD  8421  infxpenc2lem2OLD  8422  infxpenc2OLD  8424  ackbij2lem2  8641  ackbij2  8644  canthp1lem2  9052  pwfseqlem5  9062  pwfseq  9063  seqf1olem2  12147  seqf1o  12148  hasheqf1oi  12424  hashf1rn  12425  hashfacen  12503  wrd2f1tovbij  12898  summo  13539  fsum  13542  ackbijnn  13640  prodmo  13743  fprod  13748  bitsf1ocnv  14094  sadcaddlem  14107  unbenlem  14426  setcinv  15417  yonffthlem  15551  grplactcnv  16138  eqgen  16254  isgim  16310  elsymgbas2  16406  symg1bas  16421  cayleyth  16440  gsumval3eu  16907  gsumval3OLD  16908  gsumval3lem1  16909  gsumval3lem2  16910  islmim  17708  coe1mul2lem2  18309  znunithash  18603  uvcendim  18882  mdet0f1o  19095  tgpconcompeqg  20610  resinf1o  22923  efif1olem4  22932  logf1o  22952  relogf1o  22954  dvlog  23032  isismt  23921  nbgraf1o0  24446  cusgrafilem3  24481  wlknwwlknbij2  24714  wlkiswwlkbij2  24721  wwlkextbij  24733  wlknwwlknvbij  24740  clwwlkbij  24799  clwwlkvbij  24801  clwlksizeeq  24852  iseupa  24965  eupares  24975  eupap1  24976  frgrancvvdeqlem9  25041  numclwlk1lem2  25097  numclwwlk2lem3  25106  hoif  26673  rabfodom  27404  fcobijfs  27549  fpwrelmapffs  27557  indf1o  28037  eulerpartlem1  28306  eulerpartgbij  28311  eulerpart  28321  derangenlem  28615  subfacp1lem2a  28624  subfacp1lem3  28626  subfacp1lem5  28628  subfacp1lem6  28629  subfacp1  28630  elgiso  29036  isismty  30297  ismrer1  30334  isrngoiso  30381  eldioph2lem1  30693  pwfi2f1o  31044  equivestrcsetc  32658  islaut  35807  ispautN  35823  hvmap1o  37490

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-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-opab 4511  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600