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  24181  dfon2lem8  24217  dfon2lem9  24218  19.12b  24229  predreseq  24250  dffr4  24253  brtxpsd3  24507  dfom5b  24523  dffun10  24524  elfuns  24525  mptelee  24595  fates  25058  pm11.53g  25067  difeqri2  25143  prcnt  25654  heibor1lem  26636  n0el  26828  ralxpxfr2d  26863  dford4  27225  pm10.541  27665  pm10.542  27666  2exnaln  27675  19.21vv  27677  19.31vv  27685  19.28vv  27687  pm11.62  27696  ax10ext  27709  pm13.196a  27717  2sbc6g  27718  elnev  27741  conss34  27748  2rexsb  28051  2rmoswap  28065  hbexgVD  28998  bnj89  29063  bnj115  29067  bnj145  29071  bnj538  29085  bnj1143  29138  bnj110  29206  bnj611  29266  bnj864  29270  bnj865  29271  bnj1000  29289  bnj978  29297  bnj1049  29320  bnj1052  29321  bnj1090  29325  bnj1030  29333  bnj1133  29335  bnj1171  29346  bnj1172  29347  bnj1174  29349  bnj1176  29351  bnj1204  29358  bnj1253  29363  bnj1388  29379  bnj1523  29417  dvelimhwNEW7  29432  ax12olem2wAUX7  29433  equsalNEW7  29464  dvelimhvAUX7  29469  sbcomwAUX7  29562  sb8ewAUX7  29566  sbnf2NEW7  29580  2sb6NEW7  29582  sb6aNEW7  29583  sbexNEW7  29589  sbalvNEW7  29590  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