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

Theorem albii 1557
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 1555 . 2  |-  ( A. x ( ph  <->  ps )  ->  ( A. x ph  <->  A. x ps ) )
2 albii.1 . 2  |-  ( ph  <->  ps )
31, 2mpg 1539 1  |-  ( A. x ph  <->  A. x ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 176   A.wal 1531
This theorem is referenced by:  2albii  1558  hbxfrbi  1559  nfbii  1560  alex  1563  2nalexn  1564  alinexa  1569  alexn  1570  19.26-2  1585  19.26-3an  1586  19.35  1591  19.30  1595  19.43OLD  1597  albiim  1602  2albiim  1603  exintrbi  1604  19.8wOLD  1684  alrot3  1729  alrot4  1730  hba1  1745  equsalhw  1755  equsalhwOLD  1756  dvelimhw  1761  19.21-2  1823  19.32  1842  19.31  1843  aaan  1856  19.23vv  1864  pm11.53  1865  19.12vv  1870  ax12olem2  1900  equsal  1932  dvelimh  1936  sbcom  2061  sb8e  2065  sbnf2  2080  2sb6  2085  sbcom2  2086  sb6a  2088  2sb6rf  2090  sbex  2100  sbalv  2101  2exsb  2104  dvelimALT  2105  sbal2  2106  dvelimf-o  2152  ax10-16  2162  sb8eu  2194  eu1  2197  eu2  2201  moanim  2232  2mo  2254  2eu3  2258  2eu4  2259  exists1  2265  eqcom  2318  hblem  2420  abeq2  2421  abeq1  2422  nfceqi  2448  abid2f  2477  ralbii2  2605  r2alf  2612  r3al  2634  r19.21t  2662  r19.23t  2691  rabid2  2751  rabbi  2752  ralv  2835  ceqsralt  2845  ralab  2960  ralrab2  2965  euind  2986  reu2  2987  reu3  2989  rmo4  2992  reu8  2995  rmoim  2998  2reuswap  3001  reuind  3002  2reu5lem2  3005  2reu5lem3  3006  ra5  3109  rmo2  3110  rmo3  3112  dfss2  3203  ss2ab  3275  ss2rab  3283  rabss  3284  uniiunlem  3294  ssequn1  3379  unss  3383  ralunb  3390  ssin  3425  n0f  3497  eqv  3504  disj  3529  disj3  3533  ssdif0  3547  inssdif0  3555  ssundif  3571  pwss  3673  ralsns  3704  disjsn  3727  euabsn2  3732  snss  3782  pwpw0  3800  pwsnALT  3859  dfnfc2  3882  unissb  3894  elintrab  3911  ssintrab  3922  intun  3931  intpr  3932  dfiin2g  3973  iunss  3980  dfdisj2  4032  cbvdisj  4040  nfdisj  4042  disjor  4044  invdisj  4049  dftr2  4152  dftr5  4153  trint  4165  axrep1  4169  axrep5  4173  axsep  4177  zfnuleu  4183  axnulALT  4184  vprc  4189  inex1  4192  axpweq  4224  zfpow  4226  axpow2  4227  axpow3  4228  nfnid  4241  dtruALT  4244  zfpair2  4252  dtruALT2  4256  ssextss  4264  moabex  4269  dffr2  4395  dfepfr  4415  sucel  4502  zfun  4550  uniex2  4552  reusv2lem4  4575  frinxp  4792  ssrel  4813  eqrelrel  4825  reliun  4843  raliunxp  4862  relop  4871  dmopab3  4928  dm0rn0  4932  reldm0  4933  dffr3  5082  cotr  5092  issref  5093  asymref  5096  asymref2  5097  intirr  5098  sb8iota  5263  dffun2  5302  dffun3  5303  dffun4  5304  dffun5  5305  dffun6f  5306  dffun7  5317  funopab  5324  funcnv2  5346  funcnv  5347  fun2cnv  5349  fun11  5352  fununi  5353  funcnvuni  5354  fnres  5397  fnopabg  5404  brprcneu  5556  dffv2  5630  dff13  5825  eqoprab2b  5948  mpt22eqb  5995  ralrnmpt2  6000  tfrlem2  6434  dfer2  6703  fiint  7178  marypha1lem  7231  marypha2lem3  7235  inf2  7369  axinf2  7386  scottexs  7602  scott0s  7603  aceq1  7789  dfac4  7794  dfac7  7803  dfac0  7804  dfac1  7805  dfac10  7808  dfac10c  7809  dfac10b  7810  kmlem4  7824  kmlem12  7832  kmlem14  7834  kmlem15  7835  kmlem16  7836  dfackm  7837  ac6n  8157  axpowndlem3  8266  zfcndrep  8281  zfcndun  8282  zfcndpow  8283  axgroth5  8491  axgroth2  8492  grothpw  8493  axgroth4  8499  grothprim  8501  sstskm  8509  fimaxre3  9748  infm3  9758  nnwos  10333  rpnnen2  12551  isprm2  12813  vdwmc2  13073  pgpfac1  15364  pgpfac  15368  iunocv  16637  2ndcdisj2  17239  hausdiag  17395  rnelfmlem  17699  alexsubALTlem3  17795  itg2leub  19142  nmoubi  21405  nmobndseqi  21412  nmobndseqiOLD  21413  isch2  21858  isch3  21876  choc0  21960  nmopub  22543  nmfnleub  22560  xfree2  23080  abeq2f  23090  rabid2f  23097  mo5f  23108  nmo  23109  2reuswap2  23111  rmo3f  23118  rmo4fOLD  23119  cbvdisjf  23158  disjorf  23164  mptfnf  23223  funcnvmptOLD  23231  funcnvmpt  23232  funcnv5mpt  23233  cnextfun  23414  rrhfun  23575  ballotlem2  23920  axrepprim  24332  axunprim  24333  axpowprim  24334  axinfprim  24336  axacprim  24337  untuni  24339  dffr5  24495  dfon2lem8  24531  dfon2lem9  24532  19.12b  24543  predreseq  24564  dffr4  24567  brtxpsd3  24821  dfom5b  24837  dffun10  24838  elfuns  24839  mptelee  24909  heibor1lem  25681  n0el  25873  ralxpxfr2d  25908  dford4  26270  pm10.541  26710  pm10.542  26711  2exnaln  26720  19.21vv  26722  19.31vv  26730  19.28vv  26732  pm11.62  26741  ax10ext  26754  pm13.196a  26762  2sbc6g  26763  elnev  26786  conss34  26793  2rexsb  27096  2rmoswap  27110  hbexgVD  28193  bnj89  28258  bnj115  28262  bnj145  28266  bnj538  28280  bnj1143  28333  bnj110  28401  bnj611  28461  bnj864  28465  bnj865  28466  bnj1000  28484  bnj978  28492  bnj1049  28515  bnj1052  28516  bnj1090  28520  bnj1030  28528  bnj1133  28530  bnj1171  28541  bnj1172  28542  bnj1174  28544  bnj1176  28546  bnj1204  28553  bnj1253  28558  bnj1388  28574  bnj1523  28612  dvelimhwNEW7  28627  ax12olem2wAUX7  28628  equsalNEW7  28659  dvelimhvAUX7  28664  sbcomwAUX7  28757  sb8ewAUX7  28761  sbnf2NEW7  28775  2sb6NEW7  28777  sb6aNEW7  28778  sbexNEW7  28784  sbalvNEW7  28785  dvelimALTNEW7  28803  alrot3OLD7  28832  alrot4OLD7  28833  aaanOLD7  28848  pm11.53OLD7  28850  19.12vvOLD7  28851  ax12olem2OLD7  28856  dvelimhOLD7  28863  sbcomOLD7  28905  sb8eOLD7  28907  sbcom2OLD7  28911  2sb6rfOLD7  28914  2exsbOLD7  28919  sbal2OLD7  28920  ax12-4  28924  a12study4  28935  dvelimfALT2OLD  28943  a12lem2  28949  a12studyALT  28951  a12study10  28954  a12study10n  28955  pmapglbx  29776
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator