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

Theorem albii 1575
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 1573 . 2  |-  ( A. x ( ph  <->  ps )  ->  ( A. x ph  <->  A. x ps ) )
2 albii.1 . 2  |-  ( ph  <->  ps )
31, 2mpg 1557 1  |-  ( A. x ph  <->  A. x ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 177   A.wal 1549
This theorem is referenced by:  2albii  1576  hbxfrbi  1577  nfbii  1578  alex  1581  2nalexn  1582  alinexa  1588  alexn  1589  19.26-2  1604  19.26-3an  1605  19.35  1610  19.30  1614  19.43OLD  1616  albiim  1621  2albiim  1622  exintrbi  1623  19.8wOLD  1705  alrot3  1753  alrot4  1754  equsalhw  1860  equsalhwOLD  1861  dvelimhwOLD  1877  19.21-2  1887  19.32  1896  19.31  1897  aaan  1906  19.23vv  1915  pm11.53  1916  19.12vv  1921  equsal  1999  equsalOLD  2000  ax12olem2OLD  2012  dvelimhOLD  2072  sbcomOLD  2165  sbnf2  2184  2sb6  2189  sbcom2  2190  sb6a  2193  2sb6rf  2195  sbex  2205  sbalv  2206  2exsb  2209  dvelimALT  2210  sbal2  2211  dvelimf-o  2257  ax10-16  2267  sb8eu  2299  eu1  2302  eu2  2306  moanim  2337  2mo  2359  2eu3  2363  2eu4  2364  exists1  2370  eqcom  2438  hblem  2540  abeq2  2541  abeq1  2542  nfceqi  2568  abid2f  2597  ralbii2  2733  r2alf  2740  r3al  2763  r19.21t  2791  r19.23t  2820  rabid2  2885  rabbi  2886  ralv  2969  ceqsralt  2979  ralab  3095  ralrab2  3100  euind  3121  reu2  3122  reu3  3124  rmo4  3127  reu8  3130  rmoim  3133  2reuswap  3136  reuind  3137  2reu5lem2  3140  2reu5lem3  3141  ra5  3245  rmo2  3246  rmo3  3248  dfss2  3337  ss2ab  3411  ss2rab  3419  rabss  3420  uniiunlem  3431  ssequn1  3517  unss  3521  ralunb  3528  ssin  3563  n0f  3636  eqv  3643  disj  3668  disj3  3672  ssdif0  3686  inssdif0  3695  ssundif  3711  pwss  3813  ralsns  3844  disjsn  3868  euabsn2  3875  snss  3926  pwpw0  3946  pwsnALT  4010  dfnfc2  4033  unissb  4045  elintrab  4062  ssintrab  4073  intun  4082  intpr  4083  dfiin2g  4124  iunss  4132  dfdisj2  4184  cbvdisj  4192  disjor  4196  dftr2  4304  dftr5  4305  trint  4317  axrep1  4321  axrep5  4325  axsep  4329  zfnuleu  4335  axnulALT  4336  vprc  4341  inex1  4344  axpweq  4376  zfpow  4378  axpow2  4379  axpow3  4380  nfnid  4393  dtruALT  4396  zfpair2  4404  dtruALT2  4408  ssextss  4417  moabex  4422  dffr2  4547  dfepfr  4567  sucel  4654  zfun  4702  uniex2  4704  reusv2lem4  4727  frinxp  4943  ssrel  4964  ssrel2  4966  eqrelrel  4977  reliun  4995  raliunxp  5014  relop  5023  dmopab3  5082  dm0rn0  5086  reldm0  5087  dffr3  5236  cotr  5246  issref  5247  asymref  5250  asymref2  5251  intirr  5252  sb8iota  5425  dffun2  5464  dffun3  5465  dffun4  5466  dffun5  5467  dffun6f  5468  dffun7  5479  funopab  5486  funcnv2  5510  funcnv  5511  fun2cnv  5513  fun11  5516  fununi  5517  funcnvuni  5518  fnres  5561  fnopabg  5568  brprcneu  5721  dffv2  5796  dff13  6004  eqoprab2b  6132  mpt22eqb  6179  ralrnmpt2  6184  tfrlem2  6637  dfer2  6906  fiint  7383  marypha1lem  7438  marypha2lem3  7442  inf2  7578  axinf2  7595  scottexs  7811  scott0s  7812  aceq1  7998  dfac4  8003  dfac7  8012  dfac0  8013  dfac1  8014  dfac10  8017  dfac10c  8018  dfac10b  8019  kmlem4  8033  kmlem12  8041  kmlem14  8043  kmlem15  8044  kmlem16  8045  dfackm  8046  ac6n  8365  axpowndlem3  8474  zfcndrep  8489  zfcndun  8490  zfcndpow  8491  axgroth5  8699  axgroth2  8700  grothpw  8701  axgroth4  8707  grothprim  8709  sstskm  8717  fimaxre3  9957  infm3  9967  nnwos  10544  rpnnen2  12825  isprm2  13087  vdwmc2  13347  pgpfac1  15638  pgpfac  15642  iunocv  16908  2ndcdisj2  17520  hausdiag  17677  rnelfmlem  17984  alexsubALTlem3  18080  cnextfun  18095  itg2leub  19626  nmoubi  22273  nmobndseqi  22280  nmobndseqiOLD  22281  isch2  22726  isch3  22744  choc0  22828  nmopub  23411  nmfnleub  23428  xfree2  23948  abeq2f  23960  rabid2f  23967  mo5f  23972  nmo  23973  2reuswap2  23975  rmo3f  23982  rmo4fOLD  23983  cbvdisjf  24015  disjorf  24021  mptfnf  24073  funcnvmptOLD  24082  funcnvmpt  24083  funcnv5mpt  24084  ballotlem2  24746  axrepprim  25151  axunprim  25152  axpowprim  25153  axinfprim  25155  axacprim  25156  untuni  25158  dffr5  25376  dfon2lem8  25417  dfon2lem9  25418  19.12b  25429  predreseq  25454  dffr4  25457  brtxpsd3  25741  dfom5b  25757  dffun10  25759  mptelee  25834  heibor1lem  26518  n0el  26708  ralxpxfr2d  26741  dford4  27100  pm10.541  27539  pm10.542  27540  2exnaln  27549  19.21vv  27551  19.31vv  27559  19.28vv  27561  pm11.62  27570  ax10ext  27583  pm13.196a  27591  2sbc6g  27592  elnev  27615  conss34  27621  2rexsb  27924  2rmoswap  27938  hbexgVD  29018  bnj89  29086  bnj115  29090  bnj145  29094  bnj538  29108  bnj1143  29161  bnj110  29229  bnj611  29289  bnj864  29293  bnj865  29294  bnj1000  29312  bnj978  29320  bnj1049  29343  bnj1052  29344  bnj1090  29348  bnj1030  29356  bnj1133  29358  bnj1171  29369  bnj1172  29370  bnj1174  29372  bnj1176  29374  bnj1204  29381  bnj1253  29386  bnj1388  29402  bnj1523  29440  dvelimhwNEW7  29455  ax12olem2wAUX7  29456  equsalNEW7  29487  dvelimhvAUX7  29492  sbcomwAUX7  29588  sb8ewAUX7  29594  sbnf2NEW7  29608  2sb6NEW7  29610  sb6aNEW7  29611  sbexNEW7  29617  sbalvNEW7  29618  dvelimALTNEW7  29636  sbcom2NEW7  29644  ax7w15lemxAUX7  29666  ax7w15lemAUX7  29667  ax7w14lemAUX7  29669  alrot3OLD7  29682  alrot4OLD7  29683  aaanOLD7  29698  pm11.53OLD7  29700  19.12vvOLD7  29701  ax12olem2OLD7  29706  dvelimhOLD7  29713  sbcomOLD7  29755  sb8eOLD7  29757  2sb6rfOLD7  29762  2exsbOLD7  29767  sbal2OLD7  29768  pmapglbx  30566
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator