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

Theorem f1oeq1 6768
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 6729 . . 3 (𝐹 = 𝐺 → (𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵))
2 foeq1 6748 . . 3 (𝐹 = 𝐺 → (𝐹:𝐴onto𝐵𝐺:𝐴onto𝐵))
31, 2anbi12d 632 . 2 (𝐹 = 𝐺 → ((𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵) ↔ (𝐺:𝐴1-1𝐵𝐺:𝐴onto𝐵)))
4 df-f1o 6499 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵))
5 df-f1o 6499 . 2 (𝐺:𝐴1-1-onto𝐵 ↔ (𝐺:𝐴1-1𝐵𝐺:𝐴onto𝐵))
63, 4, 53bitr4g 314 1 (𝐹 = 𝐺 → (𝐹:𝐴1-1-onto𝐵𝐺:𝐴1-1-onto𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  1-1wf1 6489  ontowfo 6490  1-1-ontowf1o 6491
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3407  df-v 3446  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-sn 4586  df-pr 4588  df-op 4592  df-br 5105  df-opab 5167  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499
This theorem is referenced by:  f1oeq123d  6774  f1oeq1d  6775  f1ocnvb  6793  resin  6802  f1ovi  6819  f1oresrab  7068  fsn  7076  fveqf1o  7244  isoeq1  7257  f1oexbi  7856  oacomf1o  8480  mapsnd  8758  mapsnf1o3  8767  f1oen4g  8838  f1oen3g  8840  en0  8891  en0OLD  8892  en0r  8894  ensn1  8895  ensn1OLD  8896  en2sn  8919  en2snOLD  8920  en2prd  8926  xpcomf1o  8939  omf1o  8953  enfixsn  8959  domss2  9014  ssfiALT  9052  php3  9090  php3OLD  9102  isinf  9138  isinfOLD  9139  oef1o  9568  cnfcom  9570  cnfcom3  9574  infxpenc  9888  ackbij2lem2  10110  ackbij2  10113  canthp1lem2  10523  pwfseqlem5  10533  seqf1olem2  13877  seqf1o  13878  hasheqf1oi  14179  hashf1rn  14180  hasheqf1od  14181  hashfacen  14279  hashfacenOLD  14280  wrd2f1tovbij  14783  summo  15537  fsum  15540  ackbijnn  15648  prodmo  15754  fprod  15759  sadcaddlem  16272  unbenlem  16715  setcinv  17911  equivestrcsetc  17975  isgim  18984  symgval  19082  elsymgbas2  19086  symg1bas  19104  cayleyth  19129  gsumval3eu  19610  gsumval3lem1  19611  gsumval3lem2  19612  islmim  20446  uvcendim  21176  coe1mul2lem2  21561  mdet0f1o  21864  resinf1o  25814  efif1olem4  25823  logf1o  25842  relogf1o  25844  dvlog  25928  2lgslem1  26664  isismt  27262  nbusgrf1o1  28104  cusgrfilem3  28191  wwlksnextbij  28633  wlksnwwlknvbij  28639  clwwlkvbij  28843  hoif  30482  rabfodom  31217  fresf1o  31330  fpwrelmapffs  31433  pmtridf1o  31725  cycpmconjslem2  31786  eulerpartlem1  32728  eulerpartgbij  32733  eulerpart  32743  derangenlem  33526  subfacp1lem2a  33535  subfacp1lem3  33537  subfacp1lem5  33539  subfacp1lem6  33540  subfacp1  33541  f1omptsn  35694  poimirlem3  35967  poimirlem4  35968  poimirlem5  35969  poimirlem6  35970  poimirlem7  35971  poimirlem8  35972  poimirlem9  35973  poimirlem10  35974  poimirlem11  35975  poimirlem12  35976  poimirlem13  35977  poimirlem14  35978  poimirlem15  35979  poimirlem16  35980  poimirlem17  35981  poimirlem18  35982  poimirlem19  35983  poimirlem20  35984  poimirlem21  35985  poimirlem22  35986  poimirlem25  35989  poimirlem26  35990  poimirlem27  35991  poimirlem29  35993  poimirlem31  35995  isismty  36146  isrngoiso  36323  islaut  38432  ispautN  38448  sticksstones4  40443  sticksstones20  40460  eldioph2lem1  40917  pwfi2f1o  41257  rfovcnvf1od  42007  clsneif1o  42109  neicvgf1o  42119  fundcmpsurbijinjpreimafv  45299  sprbisymrel  45391  prproropen  45400  isomgreqve  45717  isomushgr  45718  isomuspgrlem2  45725  isomgrsym  45728  isomgrtr  45731  ushrisomgr  45733  uspgrbispr  45753  uspgrbisymrelALT  45757  1aryenef  46431  2aryenef  46442  rrx2xpreen  46505  thincciso  46769
  Copyright terms: Public domain W3C validator