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

Theorem f1oeq1 6767
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 6728 . . 3 (𝐹 = 𝐺 → (𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵))
2 foeq1 6747 . . 3 (𝐹 = 𝐺 → (𝐹:𝐴onto𝐵𝐺:𝐴onto𝐵))
31, 2anbi12d 631 . 2 (𝐹 = 𝐺 → ((𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵) ↔ (𝐺:𝐴1-1𝐵𝐺:𝐴onto𝐵)))
4 df-f1o 6498 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵))
5 df-f1o 6498 . 2 (𝐺:𝐴1-1-onto𝐵 ↔ (𝐺:𝐴1-1𝐵𝐺:𝐴onto𝐵))
63, 4, 53bitr4g 313 1 (𝐹 = 𝐺 → (𝐹:𝐴1-1-onto𝐵𝐺:𝐴1-1-onto𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  1-1wf1 6488  ontowfo 6489  1-1-ontowf1o 6490
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3406  df-v 3445  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5166  df-rel 5637  df-cnv 5638  df-co 5639  df-dm 5640  df-rn 5641  df-fun 6493  df-fn 6494  df-f 6495  df-f1 6496  df-fo 6497  df-f1o 6498
This theorem is referenced by:  f1oeq123d  6773  f1oeq1d  6774  f1ocnvb  6792  resin  6801  f1ovi  6818  f1oresrab  7067  fsn  7075  fveqf1o  7243  isoeq1  7256  f1oexbi  7855  oacomf1o  8479  mapsnd  8757  mapsnf1o3  8766  f1oen4g  8837  f1oen3g  8839  en0  8890  en0OLD  8891  en0r  8893  ensn1  8894  ensn1OLD  8895  en2sn  8918  en2snOLD  8919  en2prd  8925  xpcomf1o  8938  omf1o  8952  enfixsn  8958  domss2  9013  ssfiALT  9051  php3  9089  php3OLD  9101  isinf  9137  isinfOLD  9138  oef1o  9567  cnfcom  9569  cnfcom3  9573  infxpenc  9887  ackbij2lem2  10109  ackbij2  10112  canthp1lem2  10522  pwfseqlem5  10532  seqf1olem2  13876  seqf1o  13877  hasheqf1oi  14178  hashf1rn  14179  hasheqf1od  14180  hashfacen  14278  hashfacenOLD  14279  wrd2f1tovbij  14782  summo  15536  fsum  15539  ackbijnn  15647  prodmo  15753  fprod  15758  sadcaddlem  16271  unbenlem  16714  setcinv  17910  equivestrcsetc  17974  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  27274  nbusgrf1o1  28116  cusgrfilem3  28203  wwlksnextbij  28645  wlksnwwlknvbij  28651  clwwlkvbij  28855  hoif  30494  rabfodom  31229  fresf1o  31342  fpwrelmapffs  31445  pmtridf1o  31737  cycpmconjslem2  31798  eulerpartlem1  32740  eulerpartgbij  32745  eulerpart  32755  derangenlem  33538  subfacp1lem2a  33547  subfacp1lem3  33549  subfacp1lem5  33551  subfacp1lem6  33552  subfacp1  33553  f1omptsn  35703  poimirlem3  35976  poimirlem4  35977  poimirlem5  35978  poimirlem6  35979  poimirlem7  35980  poimirlem8  35981  poimirlem9  35982  poimirlem10  35983  poimirlem11  35984  poimirlem12  35985  poimirlem13  35986  poimirlem14  35987  poimirlem15  35988  poimirlem16  35989  poimirlem17  35990  poimirlem18  35991  poimirlem19  35992  poimirlem20  35993  poimirlem21  35994  poimirlem22  35995  poimirlem25  35998  poimirlem26  35999  poimirlem27  36000  poimirlem29  36002  poimirlem31  36004  isismty  36155  isrngoiso  36332  islaut  38441  ispautN  38457  sticksstones4  40452  sticksstones20  40469  eldioph2lem1  40948  pwfi2f1o  41288  rfovcnvf1od  42038  clsneif1o  42140  neicvgf1o  42150  fundcmpsurbijinjpreimafv  45348  sprbisymrel  45440  prproropen  45449  isomgreqve  45766  isomushgr  45767  isomuspgrlem2  45774  isomgrsym  45777  isomgrtr  45780  ushrisomgr  45782  uspgrbispr  45802  uspgrbisymrelALT  45806  1aryenef  46480  2aryenef  46491  rrx2xpreen  46554  thincciso  46818
  Copyright terms: Public domain W3C validator