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

Theorem f1oeq1 5789
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 5758 . . 3  |-  ( F  =  G  ->  ( F : A -1-1-> B  <->  G : A -1-1-> B ) )
2 foeq1 5773 . . 3  |-  ( F  =  G  ->  ( F : A -onto-> B  <->  G : A -onto-> B ) )
31, 2anbi12d 709 . 2  |-  ( F  =  G  ->  (
( F : A -1-1-> B  /\  F : A -onto-> B )  <->  ( G : A -1-1-> B  /\  G : A -onto-> B ) ) )
4 df-f1o 5575 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  F : A -onto-> B ) )
5 df-f1o 5575 . 2  |-  ( G : A -1-1-onto-> B  <->  ( G : A -1-1-> B  /\  G : A -onto-> B ) )
63, 4, 53bitr4g 288 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 184    /\ wa 367    = wceq 1405   -1-1->wf1 5565   -onto->wfo 5566   -1-1-onto->wf1o 5567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-rab 2762  df-v 3060  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-br 4395  df-opab 4453  df-rel 4829  df-cnv 4830  df-co 4831  df-dm 4832  df-rn 4833  df-fun 5570  df-fn 5571  df-f 5572  df-f1 5573  df-fo 5574  df-f1o 5575
This theorem is referenced by:  f1oeq123d  5795  f1ocnvb  5811  f1orescnv  5813  resin  5819  f1ovi  5834  f1osng  5836  f1oresrab  6041  fsn  6047  fveqf1o  6187  isoeq1  6197  f1oexbi  6733  oacomf1o  7250  mapsn  7497  mapsnf1o3  7504  f1oen3g  7568  ensn1  7616  xpcomf1o  7643  omf1o  7657  enfixsn  7663  domss2  7713  php3  7740  isinf  7767  ssfi  7774  oef1o  8172  oef1oOLD  8173  cnfcomlem  8174  cnfcom  8175  cnfcom2  8177  cnfcom3  8179  cnfcom3clem  8180  cnfcomlemOLD  8182  cnfcomOLD  8183  cnfcom2OLD  8185  cnfcom3OLD  8187  cnfcom3clemOLD  8188  infxpenc  8426  infxpenc2lem2  8428  infxpenc2  8430  infxpencOLD  8431  infxpenc2lem2OLD  8432  infxpenc2OLD  8434  ackbij2lem2  8651  ackbij2  8654  canthp1lem2  9060  pwfseqlem5  9070  pwfseq  9071  seqf1olem2  12189  seqf1o  12190  hasheqf1oi  12469  hashf1rn  12470  hashfacen  12550  wrd2f1tovbij  12952  summo  13686  fsum  13689  ackbijnn  13789  prodmo  13893  fprod  13898  bitsf1ocnv  14301  sadcaddlem  14314  unbenlem  14633  setcinv  15691  equivestrcsetc  15743  yonffthlem  15873  grplactcnv  16460  eqgen  16576  isgim  16632  elsymgbas2  16728  symg1bas  16743  cayleyth  16762  gsumval3eu  17229  gsumval3OLD  17230  gsumval3lem1  17231  gsumval3lem2  17232  islmim  18026  coe1mul2lem2  18627  znunithash  18899  uvcendim  19172  mdet0f1o  19385  tgpconcompeqg  20900  resinf1o  23213  efif1olem4  23222  logf1o  23242  relogf1o  23244  dvlog  23324  isismt  24302  nbgraf1o0  24850  cusgrafilem3  24885  wlknwwlknbij2  25118  wlkiswwlkbij2  25125  wwlkextbij  25137  wlknwwlknvbij  25144  clwwlkbij  25203  clwwlkvbij  25205  clwlksizeeq  25256  iseupa  25369  eupares  25379  eupap1  25380  frgrancvvdeqlem9  25445  numclwlk1lem2  25501  numclwwlk2lem3  25510  hoif  27072  rabfodom  27805  fresf1o  27900  fcobijfs  27982  fpwrelmapffs  27990  gsummpt2d  28209  indf1o  28457  eulerpartlem1  28798  eulerpartgbij  28803  eulerpart  28813  derangenlem  29455  subfacp1lem2a  29464  subfacp1lem3  29466  subfacp1lem5  29468  subfacp1lem6  29469  subfacp1  29470  elgiso  29875  f1omptsn  31240  isismty  31559  ismrer1  31596  isrngoiso  31643  islaut  33080  ispautN  33096  hvmap1o  34763  eldioph2lem1  35034  pwfi2f1o  35386  pwfi2f1oOLD  35387
  Copyright terms: Public domain W3C validator