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

Theorem f1oeq1 5822
Description: Equality theorem for one-to-one onto functions. (Contributed by NM, 10-Feb-1997.)
Assertion
Ref Expression
f1oeq1  |-  ( F  =  G  ->  ( F : A -1-1-onto-> B  <->  G : A -1-1-onto-> B ) )

Proof of Theorem f1oeq1
StepHypRef Expression
1 f1eq1 5791 . . 3  |-  ( F  =  G  ->  ( F : A -1-1-> B  <->  G : A -1-1-> B ) )
2 foeq1 5806 . . 3  |-  ( F  =  G  ->  ( F : A -onto-> B  <->  G : A -onto-> B ) )
31, 2anbi12d 715 . 2  |-  ( F  =  G  ->  (
( F : A -1-1-> B  /\  F : A -onto-> B )  <->  ( G : A -1-1-> B  /\  G : A -onto-> B ) ) )
4 df-f1o 5608 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  F : A -onto-> B ) )
5 df-f1o 5608 . 2  |-  ( G : A -1-1-onto-> B  <->  ( G : A -1-1-> B  /\  G : A -onto-> B ) )
63, 4, 53bitr4g 291 1  |-  ( F  =  G  ->  ( F : A -1-1-onto-> B  <->  G : A -1-1-onto-> B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    = wceq 1437   -1-1->wf1 5598   -onto->wfo 5599   -1-1-onto->wf1o 5600
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-br 4424  df-opab 4483  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608
This theorem is referenced by:  f1oeq123d  5828  f1ocnvb  5844  f1orescnv  5846  resin  5852  f1ovi  5867  f1osng  5869  f1oresrab  6070  fsn  6076  fveqf1o  6215  isoeq1  6225  f1oexbi  6757  oacomf1o  7277  mapsn  7524  mapsnf1o3  7531  f1oen3g  7595  ensn1  7643  xpcomf1o  7670  omf1o  7684  enfixsn  7690  domss2  7740  php3  7767  isinf  7794  ssfi  7801  oef1o  8211  cnfcomlem  8212  cnfcom  8213  cnfcom2  8215  cnfcom3  8217  cnfcom3clem  8218  infxpenc  8456  infxpenc2lem2  8458  infxpenc2  8460  ackbij2lem2  8677  ackbij2  8680  canthp1lem2  9085  pwfseqlem5  9095  pwfseq  9096  seqf1olem2  12259  seqf1o  12260  hasheqf1oi  12540  hashf1rn  12541  hashfacen  12621  wrd2f1tovbij  13035  summo  13782  fsum  13785  ackbijnn  13885  prodmo  13989  fprod  13994  bitsf1ocnv  14417  sadcaddlem  14430  unbenlem  14851  setcinv  15984  equivestrcsetc  16036  yonffthlem  16166  grplactcnv  16753  eqgen  16869  isgim  16925  elsymgbas2  17021  symg1bas  17036  cayleyth  17055  gsumval3eu  17537  gsumval3lem1  17538  gsumval3lem2  17539  islmim  18284  coe1mul2lem2  18860  znunithash  19133  uvcendim  19403  mdet0f1o  19616  tgpconcompeqg  21124  resinf1o  23483  efif1olem4  23492  logf1o  23512  relogf1o  23514  dvlog  23594  isismt  24577  nbgraf1o0  25172  cusgrafilem3  25207  wlknwwlknbij2  25440  wlkiswwlkbij2  25447  wwlkextbij  25459  wlknwwlknvbij  25466  clwwlkbij  25525  clwwlkvbij  25527  clwlksizeeq  25578  iseupa  25691  eupares  25701  eupap1  25702  frgrancvvdeqlem9  25767  numclwlk1lem2  25823  numclwwlk2lem3  25832  hoif  27405  rabfodom  28139  fresf1o  28233  fcobijfs  28317  fpwrelmapffs  28325  gsummpt2d  28551  indf1o  28853  eulerpartlem1  29208  eulerpartgbij  29213  eulerpart  29223  derangenlem  29902  subfacp1lem2a  29911  subfacp1lem3  29913  subfacp1lem5  29915  subfacp1lem6  29916  subfacp1  29917  elgiso  30322  f1omptsn  31703  poimirlem3  31907  poimirlem4  31908  poimirlem5  31909  poimirlem6  31910  poimirlem7  31911  poimirlem8  31912  poimirlem9  31913  poimirlem10  31914  poimirlem11  31915  poimirlem12  31916  poimirlem13  31917  poimirlem14  31918  poimirlem15  31919  poimirlem16  31920  poimirlem17  31921  poimirlem18  31922  poimirlem19  31923  poimirlem20  31924  poimirlem21  31925  poimirlem22  31926  poimirlem25  31929  poimirlem26  31930  poimirlem27  31931  poimirlem29  31933  poimirlem31  31935  isismty  32097  ismrer1  32134  isrngoiso  32181  islaut  33617  ispautN  33633  hvmap1o  35300  eldioph2lem1  35571  pwfi2f1o  35924  f1oeq1d  37410  usgredgaleord  39091  nbusgrf1o1  39208  cusgrfilem3  39274
  Copyright terms: Public domain W3C validator