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

Theorem albii 1553
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 1551 . 2  |-  ( A. x ( ph  <->  ps )  ->  ( A. x ph  <->  A. x ps ) )
2 albii.1 . 2  |-  ( ph  <->  ps )
31, 2mpg 1535 1  |-  ( A. x ph  <->  A. x ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 176   A.wal 1527
This theorem is referenced by:  2albii  1554  hbxfrbi  1555  nfbii  1556  alex  1559  2nalexn  1560  alinexa  1565  alexn  1566  19.26-2  1581  19.26-3an  1582  19.35  1587  19.30  1591  19.43OLD  1593  albiim  1598  2albiim  1599  exintrbi  1600  19.8w  1659  alrot3  1712  alrot4  1713  equsalhw  1730  dvelimhw  1735  19.21-2  1792  19.32  1811  19.31  1812  aaan  1825  19.23vv  1833  pm11.53  1834  19.12vv  1839  ax12olem2  1869  equsal  1900  dvelimh  1904  sbcom  2029  sb8e  2033  sbnf2  2047  2sb6  2052  sbcom2  2053  sb6a  2055  2sb6rf  2057  sbex  2067  sbalv  2068  2exsb  2071  dvelimALT  2072  sbal2  2073  dvelimf-o  2119  ax10-16  2129  sb8eu  2161  eu1  2164  eu2  2168  moanim  2199  2mo  2221  2eu3  2225  2eu4  2226  exists1  2232  eqcom  2285  hblem  2387  abeq2  2388  abeq1  2389  nfceqi  2415  abid2f  2444  ralbii2  2571  r2alf  2578  r3al  2600  r19.21t  2628  r19.23t  2657  rabid2  2717  rabbi  2718  ralv  2801  ceqsralt  2811  ralab  2926  ralrab2  2931  euind  2952  reu2  2953  reu3  2955  rmo4  2958  reu8  2961  rmoim  2964  2reuswap  2967  reuind  2968  2reu5lem2  2971  2reu5lem3  2972  ra5  3075  rmo2  3076  rmo3  3078  dfss2  3169  ss2ab  3241  ss2rab  3249  rabss  3250  uniiunlem  3260  ssequn1  3345  unss  3349  ralunb  3356  ssin  3391  n0f  3463  eqv  3470  disj  3495  disj3  3499  ssdif0  3513  inssdif0  3521  ssundif  3537  pwss  3639  ralsns  3670  disjsn  3693  euabsn2  3698  snss  3748  pwpw0  3763  pwsnALT  3822  dfnfc2  3845  unissb  3857  elintrab  3874  ssintrab  3885  intun  3894  intpr  3895  dfiin2g  3936  iunss  3943  dfdisj2  3995  cbvdisj  4003  nfdisj  4005  disjor  4007  invdisj  4012  dftr2  4115  dftr5  4116  trint  4128  axrep1  4132  axrep5  4136  axsep  4140  zfnuleu  4146  axnulALT  4147  vprc  4152  inex1  4155  axpweq  4187  zfpow  4189  axpow2  4190  axpow3  4191  nfnid  4204  dtruALT  4207  zfpair2  4215  dtruALT2  4219  ssextss  4227  moabex  4232  dffr2  4358  dfepfr  4378  sucel  4465  zfun  4513  uniex2  4515  reusv2lem4  4538  frinxp  4755  ssrel  4776  eqrelrel  4788  reliun  4806  raliunxp  4825  relop  4834  dmopab3  4891  dm0rn0  4895  reldm0  4896  dffr3  5045  cotr  5055  issref  5056  asymref  5059  asymref2  5060  intirr  5061  sb8iota  5226  dffun2  5265  dffun3  5266  dffun4  5267  dffun5  5268  dffun6f  5269  dffun7  5280  funopab  5287  funcnv2  5309  funcnv  5310  fun2cnv  5312  fun11  5315  fununi  5316  funcnvuni  5317  fnres  5360  fnopabg  5367  brprcneu  5518  dffv2  5592  dff13  5783  eqoprab2b  5906  mpt22eqb  5953  ralrnmpt2  5958  tfrlem2  6392  dfer2  6661  fiint  7133  marypha1lem  7186  marypha2lem3  7190  inf2  7324  axinf2  7341  scottexs  7557  scott0s  7558  aceq1  7744  dfac4  7749  dfac7  7758  dfac0  7759  dfac1  7760  dfac10  7763  dfac10c  7764  dfac10b  7765  kmlem4  7779  kmlem12  7787  kmlem14  7789  kmlem15  7790  kmlem16  7791  dfackm  7792  ac6n  8112  axpowndlem3  8221  zfcndrep  8236  zfcndun  8237  zfcndpow  8238  axgroth5  8446  axgroth2  8447  grothpw  8448  axgroth4  8454  grothprim  8456  sstskm  8464  fimaxre3  9703  infm3  9713  nnwos  10286  rpnnen2  12504  isprm2  12766  vdwmc2  13026  pgpfac1  15315  pgpfac  15319  iunocv  16581  2ndcdisj2  17183  hausdiag  17339  rnelfmlem  17647  alexsubALTlem3  17743  itg2leub  19089  nmoubi  21350  nmobndseqi  21357  nmobndseqiOLD  21358  isch2  21803  isch3  21821  choc0  21905  nmopub  22488  nmfnleub  22505  xfree2  23025  ballotlem2  23047  abeq2f  23129  rabid2f  23135  2reuswap2  23137  mo5f  23143  nmo  23144  rmo3f  23178  rmo4fOLD  23179  mptfnf  23226  funcnvmptOLD  23234  funcnvmpt  23235  funcnv5mpt  23236  cbvdisjf  23350  disjorf  23356  axrepprim  24048  axunprim  24049  axpowprim  24050  axinfprim  24052  axacprim  24053  untuni  24055  dffr5  24110  dfon2lem8  24146  dfon2lem9  24147  19.12b  24158  predreseq  24179  dffr4  24182  brtxpsd3  24436  dfom5b  24452  dffun10  24453  elfuns  24454  mptelee  24523  fates  24955  pm11.53g  24964  difeqri2  25040  prcnt  25551  heibor1lem  26533  n0el  26725  ralxpxfr2d  26760  dford4  27122  pm10.541  27562  pm10.542  27563  2exnaln  27572  19.21vv  27574  19.31vv  27582  19.28vv  27584  pm11.62  27593  ax10ext  27606  pm13.196a  27614  2sbc6g  27615  elnev  27638  conss34  27645  2rexsb  27948  2rmoswap  27962  hbexgVD  28682  bnj89  28747  bnj115  28751  bnj145  28755  bnj538  28769  bnj1143  28822  bnj110  28890  bnj611  28950  bnj864  28954  bnj865  28955  bnj1000  28973  bnj978  28981  bnj1049  29004  bnj1052  29005  bnj1090  29009  bnj1030  29017  bnj1133  29019  bnj1171  29030  bnj1172  29031  bnj1174  29033  bnj1176  29035  bnj1204  29042  bnj1253  29047  bnj1388  29063  bnj1523  29101  ax12-4  29106  a12study4  29117  dvelimfALT2OLD  29125  a12lem2  29131  a12studyALT  29133  a12study10  29136  a12study10n  29137  pmapglbx  29958
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator