MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  f1oeq1 Structured version   Visualization version   GIF version

Theorem f1oeq1 6600
Description: Equality theorem for one-to-one onto functions. (Contributed by NM, 10-Feb-1997.)
Assertion
Ref Expression
f1oeq1 (𝐹 = 𝐺 → (𝐹:𝐴1-1-onto𝐵𝐺:𝐴1-1-onto𝐵))

Proof of Theorem f1oeq1
StepHypRef Expression
1 f1eq1 6566 . . 3 (𝐹 = 𝐺 → (𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵))
2 foeq1 6582 . . 3 (𝐹 = 𝐺 → (𝐹:𝐴onto𝐵𝐺:𝐴onto𝐵))
31, 2anbi12d 630 . 2 (𝐹 = 𝐺 → ((𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵) ↔ (𝐺:𝐴1-1𝐵𝐺:𝐴onto𝐵)))
4 df-f1o 6358 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵))
5 df-f1o 6358 . 2 (𝐺:𝐴1-1-onto𝐵 ↔ (𝐺:𝐴1-1𝐵𝐺:𝐴onto𝐵))
63, 4, 53bitr4g 315 1 (𝐹 = 𝐺 → (𝐹:𝐴1-1-onto𝐵𝐺:𝐴1-1-onto𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1530  1-1wf1 6348  ontowfo 6349  1-1-ontowf1o 6350
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-rab 3151  df-v 3501  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4470  df-sn 4564  df-pr 4566  df-op 4570  df-br 5063  df-opab 5125  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-fun 6353  df-fn 6354  df-f 6355  df-f1 6356  df-fo 6357  df-f1o 6358
This theorem is referenced by:  f1oeq123d  6606  f1ocnvb  6624  f1orescnv  6626  resin  6632  f1ovi  6649  f1osng  6651  f1oresrab  6884  fsn  6892  fveqf1o  7055  isoeq1  7065  f1oexbi  7624  oacomf1o  8184  mapsnd  8442  mapsnf1o3  8451  f1oen3g  8517  ensn1  8565  xpcomf1o  8598  omf1o  8612  enfixsn  8618  domss2  8668  php3  8695  isinf  8723  ssfi  8730  oef1o  9153  cnfcomlem  9154  cnfcom  9155  cnfcom2  9157  cnfcom3  9159  cnfcom3clem  9160  infxpenc  9436  infxpenc2lem2  9438  infxpenc2  9440  ackbij2lem2  9654  ackbij2  9657  canthp1lem2  10067  pwfseqlem5  10077  pwfseq  10078  seqf1olem2  13403  seqf1o  13404  hasheqf1oi  13705  hashf1rn  13706  hasheqf1od  13707  hashfacen  13805  wrd2f1tovbij  14317  summo  15067  fsum  15070  ackbijnn  15176  prodmo  15283  fprod  15288  bitsf1ocnv  15786  sadcaddlem  15799  unbenlem  16237  setcinv  17343  equivestrcsetc  17395  yonffthlem  17525  grplactcnv  18135  eqgen  18266  isgim  18335  elsymgbas2  18432  symg1bas  18447  cayleyth  18466  gsumval3eu  18947  gsumval3lem1  18948  gsumval3lem2  18949  islmim  19757  coe1mul2lem2  20356  znunithash  20630  uvcendim  20910  mdet0f1o  21121  tgpconncompeqg  22638  resinf1o  25036  efif1olem4  25045  logf1o  25064  relogf1o  25066  dvlog  25150  2lgslem1  25887  isismt  26237  nbusgrf1o1  27069  cusgrfilem3  27156  wwlksnextbij  27597  wlksnwwlknvbij  27604  clwwlkvbij  27809  hoif  29448  rabfodom  30183  fresf1o  30294  fcobijfs  30375  fpwrelmapffs  30386  s2f1  30538  gsummpt2d  30604  pmtridf1o  30653  cycpmconjslem2  30714  indf1o  31172  eulerpartlem1  31514  eulerpartgbij  31519  eulerpart  31529  derangenlem  32305  subfacp1lem2a  32314  subfacp1lem3  32316  subfacp1lem5  32318  subfacp1lem6  32319  subfacp1  32320  f1omptsn  34490  poimirlem3  34765  poimirlem4  34766  poimirlem5  34767  poimirlem6  34768  poimirlem7  34769  poimirlem8  34770  poimirlem9  34771  poimirlem10  34772  poimirlem11  34773  poimirlem12  34774  poimirlem13  34775  poimirlem14  34776  poimirlem15  34777  poimirlem16  34778  poimirlem17  34779  poimirlem18  34780  poimirlem19  34781  poimirlem20  34782  poimirlem21  34783  poimirlem22  34784  poimirlem25  34787  poimirlem26  34788  poimirlem27  34789  poimirlem29  34791  poimirlem31  34793  isismty  34950  ismrer1  34987  isrngoiso  35127  islaut  37089  ispautN  37105  hvmap1o  38769  eldioph2lem1  39225  pwfi2f1o  39564  rfovcnvf1od  40218  clsneif1o  40322  neicvgf1o  40332  f1oeq1d  41305  sprbisymrel  43496  prproropen  43505  isomgreqve  43825  isomushgr  43826  isomuspgrlem2  43833  isomgrsym  43836  isomgrtr  43839  ushrisomgr  43841  uspgrbispr  43861  uspgrbisymrelALT  43865  rrx2xpreen  44541
  Copyright terms: Public domain W3C validator