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

Theorem albii 1556
Description: Inference adding universal quantifier to both sides of an equivalence. (Contributed by NM, 7-Aug-1994.)
Hypothesis
Ref Expression
albii.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
albii  |-  ( A. x ph  <->  A. x ps )

Proof of Theorem albii
StepHypRef Expression
1 albi 1554 . 2  |-  ( A. x ( ph  <->  ps )  ->  ( A. x ph  <->  A. x ps ) )
2 albii.1 . 2  |-  ( ph  <->  ps )
31, 2mpg 1538 1  |-  ( A. x ph  <->  A. x ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 176   A.wal 1530
This theorem is referenced by:  2albii  1557  hbxfrbi  1558  nfbii  1559  alex  1562  2nalexn  1563  alinexa  1568  alexn  1569  19.26-2  1584  19.26-3an  1585  19.35  1590  19.30  1594  19.43OLD  1596  albiim  1601  2albiim  1602  exintrbi  1603  19.8wOLD  1678  alrot3  1724  alrot4  1725  equsalhw  1742  dvelimhw  1747  19.21-2  1804  19.32  1823  19.31  1824  aaan  1837  19.23vv  1845  pm11.53  1846  19.12vv  1851  ax12olem2  1881  equsal  1913  dvelimh  1917  sbcom  2042  sb8e  2046  sbnf2  2060  2sb6  2065  sbcom2  2066  sb6a  2068  2sb6rf  2070  sbex  2080  sbalv  2081  2exsb  2084  dvelimALT  2085  sbal2  2086  dvelimf-o  2132  ax10-16  2142  sb8eu  2174  eu1  2177  eu2  2181  moanim  2212  2mo  2234  2eu3  2238  2eu4  2239  exists1  2245  eqcom  2298  hblem  2400  abeq2  2401  abeq1  2402  nfceqi  2428  abid2f  2457  ralbii2  2584  r2alf  2591  r3al  2613  r19.21t  2641  r19.23t  2670  rabid2  2730  rabbi  2731  ralv  2814  ceqsralt  2824  ralab  2939  ralrab2  2944  euind  2965  reu2  2966  reu3  2968  rmo4  2971  reu8  2974  rmoim  2977  2reuswap  2980  reuind  2981  2reu5lem2  2984  2reu5lem3  2985  ra5  3088  rmo2  3089  rmo3  3091  dfss2  3182  ss2ab  3254  ss2rab  3262  rabss  3263  uniiunlem  3273  ssequn1  3358  unss  3362  ralunb  3369  ssin  3404  n0f  3476  eqv  3483  disj  3508  disj3  3512  ssdif0  3526  inssdif0  3534  ssundif  3550  pwss  3652  ralsns  3683  disjsn  3706  euabsn2  3711  snss  3761  pwpw0  3779  pwsnALT  3838  dfnfc2  3861  unissb  3873  elintrab  3890  ssintrab  3901  intun  3910  intpr  3911  dfiin2g  3952  iunss  3959  dfdisj2  4011  cbvdisj  4019  nfdisj  4021  disjor  4023  invdisj  4028  dftr2  4131  dftr5  4132  trint  4144  axrep1  4148  axrep5  4152  axsep  4156  zfnuleu  4162  axnulALT  4163  vprc  4168  inex1  4171  axpweq  4203  zfpow  4205  axpow2  4206  axpow3  4207  nfnid  4220  dtruALT  4223  zfpair2  4231  dtruALT2  4235  ssextss  4243  moabex  4248  dffr2  4374  dfepfr  4394  sucel  4481  zfun  4529  uniex2  4531  reusv2lem4  4554  frinxp  4771  ssrel  4792  eqrelrel  4804  reliun  4822  raliunxp  4841  relop  4850  dmopab3  4907  dm0rn0  4911  reldm0  4912  dffr3  5061  cotr  5071  issref  5072  asymref  5075  asymref2  5076  intirr  5077  sb8iota  5242  dffun2  5281  dffun3  5282  dffun4  5283  dffun5  5284  dffun6f  5285  dffun7  5296  funopab  5303  funcnv2  5325  funcnv  5326  fun2cnv  5328  fun11  5331  fununi  5332  funcnvuni  5333  fnres  5376  fnopabg  5383  brprcneu  5534  dffv2  5608  dff13  5799  eqoprab2b  5922  mpt22eqb  5969  ralrnmpt2  5974  tfrlem2  6408  dfer2  6677  fiint  7149  marypha1lem  7202  marypha2lem3  7206  inf2  7340  axinf2  7357  scottexs  7573  scott0s  7574  aceq1  7760  dfac4  7765  dfac7  7774  dfac0  7775  dfac1  7776  dfac10  7779  dfac10c  7780  dfac10b  7781  kmlem4  7795  kmlem12  7803  kmlem14  7805  kmlem15  7806  kmlem16  7807  dfackm  7808  ac6n  8128  axpowndlem3  8237  zfcndrep  8252  zfcndun  8253  zfcndpow  8254  axgroth5  8462  axgroth2  8463  grothpw  8464  axgroth4  8470  grothprim  8472  sstskm  8480  fimaxre3  9719  infm3  9729  nnwos  10302  rpnnen2  12520  isprm2  12782  vdwmc2  13042  pgpfac1  15331  pgpfac  15335  iunocv  16597  2ndcdisj2  17199  hausdiag  17355  rnelfmlem  17663  alexsubALTlem3  17759  itg2leub  19105  nmoubi  21366  nmobndseqi  21373  nmobndseqiOLD  21374  isch2  21819  isch3  21837  choc0  21921  nmopub  22504  nmfnleub  22521  xfree2  23041  ballotlem2  23063  abeq2f  23145  rabid2f  23151  2reuswap2  23153  mo5f  23159  nmo  23160  rmo3f  23194  rmo4fOLD  23195  mptfnf  23241  funcnvmptOLD  23249  funcnvmpt  23250  funcnv5mpt  23251  cbvdisjf  23365  disjorf  23371  axrepprim  24063  axunprim  24064  axpowprim  24065  axinfprim  24067  axacprim  24068  untuni  24070  dffr5  24180  dfon2lem8  24216  dfon2lem9  24217  19.12b  24228  predreseq  24249  dffr4  24252  brtxpsd3  24506  dfom5b  24522  dffun10  24523  elfuns  24524  mptelee  24594  fates  25057  pm11.53g  25066  difeqri2  25142  prcnt  25653  heibor1lem  26635  n0el  26827  ralxpxfr2d  26862  dford4  27224  pm10.541  27664  pm10.542  27665  2exnaln  27674  19.21vv  27676  19.31vv  27684  19.28vv  27686  pm11.62  27695  ax10ext  27708  pm13.196a  27716  2sbc6g  27717  elnev  27740  conss34  27747  2rexsb  28050  2rmoswap  28064  hbexgVD  28997  bnj89  29062  bnj115  29066  bnj145  29070  bnj538  29084  bnj1143  29137  bnj110  29205  bnj611  29265  bnj864  29269  bnj865  29270  bnj1000  29288  bnj978  29296  bnj1049  29319  bnj1052  29320  bnj1090  29324  bnj1030  29332  bnj1133  29334  bnj1171  29345  bnj1172  29346  bnj1174  29348  bnj1176  29350  bnj1204  29357  bnj1253  29362  bnj1388  29378  bnj1523  29416  dvelimhwNEW7  29431  ax12olem2wAUX7  29432  equsalNEW7  29463  dvelimhvAUX7  29468  sbcomwAUX7  29561  sb8ewAUX7  29565  sbnf2NEW7  29579  2sb6NEW7  29581  sb6aNEW7  29582  sbexNEW7  29588  sbalvNEW7  29589  dvelimALTNEW7  29607  alrot3OLD7  29636  alrot4OLD7  29637  aaanOLD7  29652  pm11.53OLD7  29654  19.12vvOLD7  29655  ax12olem2OLD7  29660  dvelimhOLD7  29667  sbcomOLD7  29709  sb8eOLD7  29711  sbcom2OLD7  29715  2sb6rfOLD7  29718  2exsbOLD7  29723  sbal2OLD7  29724  ax12-4  29728  a12study4  29739  dvelimfALT2OLD  29747  a12lem2  29753  a12studyALT  29755  a12study10  29758  a12study10n  29759  pmapglbx  30580
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator