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

Theorem f1oeq1 5463
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 5432 . . 3  |-  ( F  =  G  ->  ( F : A -1-1-> B  <->  G : A -1-1-> B ) )
2 foeq1 5447 . . 3  |-  ( F  =  G  ->  ( F : A -onto-> B  <->  G : A -onto-> B ) )
31, 2anbi12d 691 . 2  |-  ( F  =  G  ->  (
( F : A -1-1-> B  /\  F : A -onto-> B )  <->  ( G : A -1-1-> B  /\  G : A -onto-> B ) ) )
4 df-f1o 5262 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  F : A -onto-> B ) )
5 df-f1o 5262 . 2  |-  ( G : A -1-1-onto-> B  <->  ( G : A -1-1-> B  /\  G : A -onto-> B ) )
63, 4, 53bitr4g 279 1  |-  ( F  =  G  ->  ( F : A -1-1-onto-> B  <->  G : A -1-1-onto-> B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1623   -1-1->wf1 5252   -onto->wfo 5253   -1-1-onto->wf1o 5254
This theorem is referenced by:  f1oeq123d  5469  f1ocnvb  5486  f1orescnv  5488  resin  5495  f1ovi  5512  f1osng  5514  f1oprswap  5515  fsn  5696  fveqf1o  5806  isoeq1  5816  oacomf1o  6563  mapsn  6809  mapsnf1o3  6816  f1oen3g  6877  ensn1  6925  xpcomf1o  6951  omf1o  6965  domss2  7020  php3  7047  isinf  7076  ssfi  7083  oef1o  7401  cnfcomlem  7402  cnfcom  7403  cnfcom2  7405  cnfcom3  7407  cnfcom3clem  7408  infxpenc  7645  infxpenc2lem2  7647  infxpenc2  7649  ackbij2lem2  7866  ackbij2  7869  canthp1lem2  8275  pwfseqlem5  8285  pwfseq  8286  seqf1olem2  11086  seqf1o  11087  hashfacen  11392  summo  12190  fsum  12193  ackbijnn  12286  bitsf1ocnv  12635  sadcaddlem  12648  unbenlem  12955  setcinv  13922  yonffthlem  14056  grplactcnv  14564  eqgen  14670  isgim  14726  elsymgbas2  14773  cayleyth  14790  gsumval3eu  15190  gsumval3  15191  islmim  15815  coe1mul2lem2  16345  znunithash  16518  tgpconcompeqg  17794  resinf1o  19898  efif1olem4  19907  logf1o  19922  relogf1o  19924  dvlog  19998  hoif  22334  indf1o  23607  derangenlem  23702  subfacp1lem2a  23711  subfacp1lem3  23713  subfacp1lem5  23715  subfacp1lem6  23716  subfacp1  23717  iseupa  23881  eupares  23899  eupap1  23900  elgiso  24003  cbicp  25166  isoriso2  25213  gapm2  25369  trooo  25394  ltrooo  25404  rltrooo  25415  isismty  26525  ismrer1  26562  isrngoiso  26609  eldioph2lem1  26839  enfixsn  27257  pwfi2f1o  27260  islaut  30272  ispautN  30288  hvmap1o  31953
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024  df-opab 4078  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262
  Copyright terms: Public domain W3C validator