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

Theorem f1oeq1 6590
 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 6555 . . 3 (𝐹 = 𝐺 → (𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵))
2 foeq1 6572 . . 3 (𝐹 = 𝐺 → (𝐹:𝐴onto𝐵𝐺:𝐴onto𝐵))
31, 2anbi12d 633 . 2 (𝐹 = 𝐺 → ((𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵) ↔ (𝐺:𝐴1-1𝐵𝐺:𝐴onto𝐵)))
4 df-f1o 6342 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵))
5 df-f1o 6342 . 2 (𝐺:𝐴1-1-onto𝐵 ↔ (𝐺:𝐴1-1𝐵𝐺:𝐴onto𝐵))
63, 4, 53bitr4g 317 1 (𝐹 = 𝐺 → (𝐹:𝐴1-1-onto𝐵𝐺:𝐴1-1-onto𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538  –1-1→wf1 6332  –onto→wfo 6333  –1-1-onto→wf1o 6334 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-un 3863  df-in 3865  df-ss 3875  df-sn 4523  df-pr 4525  df-op 4529  df-br 5033  df-opab 5095  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342 This theorem is referenced by:  f1oeq123d  6596  f1oeq1d  6597  f1ocnvb  6615  f1orescnv  6617  resin  6623  f1ovi  6640  f1osng  6642  f1oresrab  6880  fsn  6888  fveqf1o  7051  isoeq1  7064  f1oexbi  7638  oacomf1o  8201  mapsnd  8468  mapsnf1o3  8477  f1oen3g  8543  en0  8590  ensn1  8592  en2sn  8612  xpcomf1o  8627  omf1o  8641  enfixsn  8647  domss2  8698  php3  8725  isinf  8769  ssfiOLD  8775  oef1o  9194  cnfcomlem  9195  cnfcom  9196  cnfcom2  9198  cnfcom3  9200  cnfcom3clem  9201  infxpenc  9478  infxpenc2  9482  ackbij2lem2  9700  ackbij2  9703  canthp1lem2  10113  pwfseqlem5  10123  pwfseq  10124  seqf1olem2  13460  seqf1o  13461  hasheqf1oi  13762  hashf1rn  13763  hasheqf1od  13764  hashfacen  13862  hashfacenOLD  13863  wrd2f1tovbij  14371  summo  15122  fsum  15125  ackbijnn  15231  prodmo  15338  fprod  15343  bitsf1ocnv  15843  sadcaddlem  15856  unbenlem  16299  setcinv  17416  equivestrcsetc  17468  yonffthlem  17598  grplactcnv  18269  eqgen  18400  isgim  18469  symgval  18564  elsymgbas2  18568  symg1bas  18586  cayleyth  18610  gsumval3eu  19092  gsumval3lem1  19093  gsumval3lem2  19094  islmim  19902  znunithash  20332  uvcendim  20612  coe1mul2lem2  20992  mdet0f1o  21293  tgpconncompeqg  22812  resinf1o  25227  efif1olem4  25236  logf1o  25255  relogf1o  25257  dvlog  25341  2lgslem1  26077  isismt  26427  nbusgrf1o1  27259  cusgrfilem3  27346  wwlksnextbij  27787  wlksnwwlknvbij  27793  clwwlkvbij  27997  hoif  29636  rabfodom  30373  fresf1o  30488  fcobijfs  30582  fpwrelmapffs  30593  s2f1  30743  gsummpt2d  30835  pmtridf1o  30887  cycpmconjslem2  30948  indf1o  31511  eulerpartlem1  31853  eulerpartgbij  31858  eulerpart  31868  derangenlem  32649  subfacp1lem2a  32658  subfacp1lem3  32660  subfacp1lem5  32662  subfacp1lem6  32663  subfacp1  32664  f1omptsn  35034  poimirlem3  35340  poimirlem4  35341  poimirlem5  35342  poimirlem6  35343  poimirlem7  35344  poimirlem8  35345  poimirlem9  35346  poimirlem10  35347  poimirlem11  35348  poimirlem12  35349  poimirlem13  35350  poimirlem14  35351  poimirlem15  35352  poimirlem16  35353  poimirlem17  35354  poimirlem18  35355  poimirlem19  35356  poimirlem20  35357  poimirlem21  35358  poimirlem22  35359  poimirlem25  35362  poimirlem26  35363  poimirlem27  35364  poimirlem29  35366  poimirlem31  35368  isismty  35519  ismrer1  35556  isrngoiso  35696  islaut  37659  ispautN  37675  hvmap1o  39339  eldioph2lem1  40074  pwfi2f1o  40413  rfovcnvf1od  41078  clsneif1o  41180  neicvgf1o  41190  fundcmpsurbijinjpreimafv  44292  sprbisymrel  44384  prproropen  44393  isomgreqve  44710  isomushgr  44711  isomuspgrlem2  44718  isomgrsym  44721  isomgrtr  44724  ushrisomgr  44726  uspgrbispr  44746  uspgrbisymrelALT  44750  1aryenef  45424  2aryenef  45435  rrx2xpreen  45498
 Copyright terms: Public domain W3C validator