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

Theorem albii 1572
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 1570 . 2  |-  ( A. x ( ph  <->  ps )  ->  ( A. x ph  <->  A. x ps ) )
2 albii.1 . 2  |-  ( ph  <->  ps )
31, 2mpg 1554 1  |-  ( A. x ph  <->  A. x ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 177   A.wal 1546
This theorem is referenced by:  2albii  1573  hbxfrbi  1574  nfbii  1575  alex  1578  2nalexn  1579  alinexa  1585  alexn  1586  19.26-2  1601  19.26-3an  1602  19.35  1607  19.30  1611  19.43OLD  1613  albiim  1618  2albiim  1619  exintrbi  1620  19.8wOLD  1701  alrot3  1749  alrot4  1750  equsalhw  1856  equsalhwOLD  1857  dvelimhwOLD  1873  19.21-2  1883  19.32  1892  19.31  1893  aaan  1902  19.23vv  1911  pm11.53  1912  19.12vv  1917  equsal  1966  equsalOLD  1967  ax12olem2OLD  1978  dvelimhOLD  2016  sbcom  2138  sbnf2  2157  2sb6  2162  sbcom2  2163  sb6a  2166  2sb6rf  2168  sbex  2178  sbalv  2179  2exsb  2182  dvelimALT  2183  sbal2  2184  dvelimf-o  2230  ax10-16  2240  sb8eu  2272  eu1  2275  eu2  2279  moanim  2310  2mo  2332  2eu3  2336  2eu4  2337  exists1  2343  eqcom  2406  hblem  2508  abeq2  2509  abeq1  2510  nfceqi  2536  abid2f  2565  ralbii2  2694  r2alf  2701  r3al  2723  r19.21t  2751  r19.23t  2780  rabid2  2845  rabbi  2846  ralv  2929  ceqsralt  2939  ralab  3055  ralrab2  3060  euind  3081  reu2  3082  reu3  3084  rmo4  3087  reu8  3090  rmoim  3093  2reuswap  3096  reuind  3097  2reu5lem2  3100  2reu5lem3  3101  ra5  3205  rmo2  3206  rmo3  3208  dfss2  3297  ss2ab  3371  ss2rab  3379  rabss  3380  uniiunlem  3391  ssequn1  3477  unss  3481  ralunb  3488  ssin  3523  n0f  3596  eqv  3603  disj  3628  disj3  3632  ssdif0  3646  inssdif0  3655  ssundif  3671  pwss  3773  ralsns  3804  disjsn  3828  euabsn2  3835  snss  3886  pwpw0  3906  pwsnALT  3970  dfnfc2  3993  unissb  4005  elintrab  4022  ssintrab  4033  intun  4042  intpr  4043  dfiin2g  4084  iunss  4092  dfdisj2  4144  cbvdisj  4152  disjor  4156  dftr2  4264  dftr5  4265  trint  4277  axrep1  4281  axrep5  4285  axsep  4289  zfnuleu  4295  axnulALT  4296  vprc  4301  inex1  4304  axpweq  4336  zfpow  4338  axpow2  4339  axpow3  4340  nfnid  4353  dtruALT  4356  zfpair2  4364  dtruALT2  4368  ssextss  4377  moabex  4382  dffr2  4507  dfepfr  4527  sucel  4614  zfun  4661  uniex2  4663  reusv2lem4  4686  frinxp  4902  ssrel  4923  ssrel2  4925  eqrelrel  4936  reliun  4954  raliunxp  4973  relop  4982  dmopab3  5041  dm0rn0  5045  reldm0  5046  dffr3  5195  cotr  5205  issref  5206  asymref  5209  asymref2  5210  intirr  5211  sb8iota  5384  dffun2  5423  dffun3  5424  dffun4  5425  dffun5  5426  dffun6f  5427  dffun7  5438  funopab  5445  funcnv2  5469  funcnv  5470  fun2cnv  5472  fun11  5475  fununi  5476  funcnvuni  5477  fnres  5520  fnopabg  5527  brprcneu  5680  dffv2  5755  dff13  5963  eqoprab2b  6091  mpt22eqb  6138  ralrnmpt2  6143  tfrlem2  6596  dfer2  6865  fiint  7342  marypha1lem  7396  marypha2lem3  7400  inf2  7534  axinf2  7551  scottexs  7767  scott0s  7768  aceq1  7954  dfac4  7959  dfac7  7968  dfac0  7969  dfac1  7970  dfac10  7973  dfac10c  7974  dfac10b  7975  kmlem4  7989  kmlem12  7997  kmlem14  7999  kmlem15  8000  kmlem16  8001  dfackm  8002  ac6n  8321  axpowndlem3  8430  zfcndrep  8445  zfcndun  8446  zfcndpow  8447  axgroth5  8655  axgroth2  8656  grothpw  8657  axgroth4  8663  grothprim  8665  sstskm  8673  fimaxre3  9913  infm3  9923  nnwos  10500  rpnnen2  12780  isprm2  13042  vdwmc2  13302  pgpfac1  15593  pgpfac  15597  iunocv  16863  2ndcdisj2  17473  hausdiag  17630  rnelfmlem  17937  alexsubALTlem3  18033  cnextfun  18048  itg2leub  19579  nmoubi  22226  nmobndseqi  22233  nmobndseqiOLD  22234  isch2  22679  isch3  22697  choc0  22781  nmopub  23364  nmfnleub  23381  xfree2  23901  abeq2f  23913  rabid2f  23920  mo5f  23925  nmo  23926  2reuswap2  23928  rmo3f  23935  rmo4fOLD  23936  cbvdisjf  23968  disjorf  23974  mptfnf  24026  funcnvmptOLD  24035  funcnvmpt  24036  funcnv5mpt  24037  ballotlem2  24699  axrepprim  25104  axunprim  25105  axpowprim  25106  axinfprim  25108  axacprim  25109  untuni  25111  dffr5  25324  dfon2lem8  25360  dfon2lem9  25361  19.12b  25372  predreseq  25393  dffr4  25396  brtxpsd3  25650  dfom5b  25666  dffun10  25667  elfuns  25668  mptelee  25738  heibor1lem  26408  n0el  26598  ralxpxfr2d  26631  dford4  26990  pm10.541  27430  pm10.542  27431  2exnaln  27440  19.21vv  27442  19.31vv  27450  19.28vv  27452  pm11.62  27461  ax10ext  27474  pm13.196a  27482  2sbc6g  27483  elnev  27506  conss34  27512  2rexsb  27815  2rmoswap  27829  hbexgVD  28727  bnj89  28792  bnj115  28796  bnj145  28800  bnj538  28814  bnj1143  28867  bnj110  28935  bnj611  28995  bnj864  28999  bnj865  29000  bnj1000  29018  bnj978  29026  bnj1049  29049  bnj1052  29050  bnj1090  29054  bnj1030  29062  bnj1133  29064  bnj1171  29075  bnj1172  29076  bnj1174  29078  bnj1176  29080  bnj1204  29087  bnj1253  29092  bnj1388  29108  bnj1523  29146  dvelimhwNEW7  29161  ax12olem2wAUX7  29162  equsalNEW7  29193  dvelimhvAUX7  29198  sbcomwAUX7  29291  sb8ewAUX7  29295  sbnf2NEW7  29309  2sb6NEW7  29311  sb6aNEW7  29312  sbexNEW7  29318  sbalvNEW7  29319  dvelimALTNEW7  29337  alrot3OLD7  29366  alrot4OLD7  29367  aaanOLD7  29382  pm11.53OLD7  29384  19.12vvOLD7  29385  ax12olem2OLD7  29390  dvelimhOLD7  29397  sbcomOLD7  29439  sb8eOLD7  29441  sbcom2OLD7  29445  2sb6rfOLD7  29447  2exsbOLD7  29452  sbal2OLD7  29453  pmapglbx  30251
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator