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

Theorem f1oeq1 6769
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 6730 . . 3 (𝐹 = 𝐺 → (𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵))
2 foeq1 6749 . . 3 (𝐹 = 𝐺 → (𝐹:𝐴onto𝐵𝐺:𝐴onto𝐵))
31, 2anbi12d 631 . 2 (𝐹 = 𝐺 → ((𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵) ↔ (𝐺:𝐴1-1𝐵𝐺:𝐴onto𝐵)))
4 df-f1o 6500 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵))
5 df-f1o 6500 . 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 6490  ontowfo 6491  1-1-ontowf1o 6492
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 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500
This theorem is referenced by:  f1oeq123d  6775  f1oeq1d  6776  f1ocnvb  6794  resin  6803  f1ovi  6820  f1oresrab  7069  fsn  7077  fveqf1o  7245  isoeq1  7258  f1oexbi  7857  oacomf1o  8504  mapsnd  8782  mapsnf1o3  8791  f1oen4g  8862  f1oen3g  8864  en0  8915  en0OLD  8916  en0r  8918  ensn1  8919  ensn1OLD  8920  en2sn  8943  en2snOLD  8944  en2prd  8950  xpcomf1o  8963  omf1o  8977  enfixsn  8983  domss2  9038  ssfiALT  9076  php3  9114  php3OLD  9126  isinf  9162  isinfOLD  9163  oef1o  9592  cnfcom  9594  cnfcom3  9598  infxpenc  9912  ackbij2lem2  10134  ackbij2  10137  canthp1lem2  10547  pwfseqlem5  10557  seqf1olem2  13902  seqf1o  13903  hasheqf1oi  14204  hashf1rn  14205  hasheqf1od  14206  hashfacen  14304  hashfacenOLD  14305  wrd2f1tovbij  14808  summo  15561  fsum  15564  ackbijnn  15672  prodmo  15778  fprod  15783  sadcaddlem  16296  unbenlem  16739  setcinv  17935  equivestrcsetc  17999  isgim  19010  symgval  19108  elsymgbas2  19112  symg1bas  19130  cayleyth  19155  gsumval3eu  19639  gsumval3lem1  19640  gsumval3lem2  19641  islmim  20475  uvcendim  21205  coe1mul2lem2  21590  mdet0f1o  21893  resinf1o  25843  efif1olem4  25852  logf1o  25871  relogf1o  25873  dvlog  25957  2lgslem1  26693  isismt  27304  nbusgrf1o1  28146  cusgrfilem3  28233  wwlksnextbij  28675  wlksnwwlknvbij  28681  clwwlkvbij  28885  hoif  30524  rabfodom  31259  fresf1o  31372  fpwrelmapffs  31475  pmtridf1o  31767  cycpmconjslem2  31828  eulerpartlem1  32770  eulerpartgbij  32775  eulerpart  32785  derangenlem  33568  subfacp1lem2a  33577  subfacp1lem3  33579  subfacp1lem5  33581  subfacp1lem6  33582  subfacp1  33583  f1omptsn  35739  poimirlem3  36012  poimirlem4  36013  poimirlem5  36014  poimirlem6  36015  poimirlem7  36016  poimirlem8  36017  poimirlem9  36018  poimirlem10  36019  poimirlem11  36020  poimirlem12  36021  poimirlem13  36022  poimirlem14  36023  poimirlem15  36024  poimirlem16  36025  poimirlem17  36026  poimirlem18  36027  poimirlem19  36028  poimirlem20  36029  poimirlem21  36030  poimirlem22  36031  poimirlem25  36034  poimirlem26  36035  poimirlem27  36036  poimirlem29  36038  poimirlem31  36040  isismty  36191  isrngoiso  36368  islaut  38477  ispautN  38493  sticksstones4  40488  sticksstones20  40505  eldioph2lem1  40985  pwfi2f1o  41325  rfovcnvf1od  42180  clsneif1o  42280  neicvgf1o  42290  fundcmpsurbijinjpreimafv  45493  sprbisymrel  45585  prproropen  45594  isomgreqve  45911  isomushgr  45912  isomuspgrlem2  45919  isomgrsym  45922  isomgrtr  45925  ushrisomgr  45927  uspgrbispr  45947  uspgrbisymrelALT  45951  1aryenef  46625  2aryenef  46636  rrx2xpreen  46699  thincciso  46963
  Copyright terms: Public domain W3C validator