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  1700  alrot3  1745  alrot4  1746  equsalhw  1850  equsalhwOLD  1851  dvelimhw  1861  19.21-2  1876  19.32  1885  19.31  1886  aaan  1895  19.23vv  1904  pm11.53  1905  19.12vv  1910  equsal  1959  equsalOLD  1960  ax12olem2OLD  1971  dvelimh  2008  sbcom  2124  sbnf2  2143  2sb6  2148  sbcom2  2149  sb6a  2152  2sb6rf  2154  sbex  2164  sbalv  2165  2exsb  2168  dvelimALT  2169  sbal2  2170  dvelimf-o  2216  ax10-16  2226  sb8eu  2258  eu1  2261  eu2  2265  moanim  2296  2mo  2318  2eu3  2322  2eu4  2323  exists1  2329  eqcom  2391  hblem  2493  abeq2  2494  abeq1  2495  nfceqi  2521  abid2f  2550  ralbii2  2679  r2alf  2686  r3al  2708  r19.21t  2736  r19.23t  2765  rabid2  2830  rabbi  2831  ralv  2914  ceqsralt  2924  ralab  3040  ralrab2  3045  euind  3066  reu2  3067  reu3  3069  rmo4  3072  reu8  3075  rmoim  3078  2reuswap  3081  reuind  3082  2reu5lem2  3085  2reu5lem3  3086  ra5  3190  rmo2  3191  rmo3  3193  dfss2  3282  ss2ab  3356  ss2rab  3364  rabss  3365  uniiunlem  3376  ssequn1  3462  unss  3466  ralunb  3473  ssin  3508  n0f  3581  eqv  3588  disj  3613  disj3  3617  ssdif0  3631  inssdif0  3640  ssundif  3656  pwss  3758  ralsns  3789  disjsn  3813  euabsn2  3820  snss  3871  pwpw0  3891  pwsnALT  3954  dfnfc2  3977  unissb  3989  elintrab  4006  ssintrab  4017  intun  4026  intpr  4027  dfiin2g  4068  iunss  4075  dfdisj2  4127  cbvdisj  4135  disjor  4139  dftr2  4247  dftr5  4248  trint  4260  axrep1  4264  axrep5  4268  axsep  4272  zfnuleu  4278  axnulALT  4279  vprc  4284  inex1  4287  axpweq  4319  zfpow  4321  axpow2  4322  axpow3  4323  nfnid  4336  dtruALT  4339  zfpair2  4347  dtruALT2  4351  ssextss  4360  moabex  4365  dffr2  4490  dfepfr  4510  sucel  4597  zfun  4644  uniex2  4646  reusv2lem4  4669  frinxp  4885  ssrel  4906  ssrel2  4908  eqrelrel  4919  reliun  4937  raliunxp  4956  relop  4965  dmopab3  5024  dm0rn0  5028  reldm0  5029  dffr3  5178  cotr  5188  issref  5189  asymref  5192  asymref2  5193  intirr  5194  sb8iota  5367  dffun2  5406  dffun3  5407  dffun4  5408  dffun5  5409  dffun6f  5410  dffun7  5421  funopab  5428  funcnv2  5452  funcnv  5453  fun2cnv  5455  fun11  5458  fununi  5459  funcnvuni  5460  fnres  5503  fnopabg  5510  brprcneu  5663  dffv2  5737  dff13  5945  eqoprab2b  6073  mpt22eqb  6120  ralrnmpt2  6125  tfrlem2  6575  dfer2  6844  fiint  7321  marypha1lem  7375  marypha2lem3  7379  inf2  7513  axinf2  7530  scottexs  7746  scott0s  7747  aceq1  7933  dfac4  7938  dfac7  7947  dfac0  7948  dfac1  7949  dfac10  7952  dfac10c  7953  dfac10b  7954  kmlem4  7968  kmlem12  7976  kmlem14  7978  kmlem15  7979  kmlem16  7980  dfackm  7981  ac6n  8300  axpowndlem3  8409  zfcndrep  8424  zfcndun  8425  zfcndpow  8426  axgroth5  8634  axgroth2  8635  grothpw  8636  axgroth4  8642  grothprim  8644  sstskm  8652  fimaxre3  9891  infm3  9901  nnwos  10478  rpnnen2  12754  isprm2  13016  vdwmc2  13276  pgpfac1  15567  pgpfac  15571  iunocv  16833  2ndcdisj2  17443  hausdiag  17600  rnelfmlem  17907  alexsubALTlem3  18003  cnextfun  18018  itg2leub  19495  nmoubi  22123  nmobndseqi  22130  nmobndseqiOLD  22131  isch2  22576  isch3  22594  choc0  22678  nmopub  23261  nmfnleub  23278  xfree2  23798  abeq2f  23806  rabid2f  23813  mo5f  23818  nmo  23819  2reuswap2  23821  rmo3f  23828  rmo4fOLD  23829  cbvdisjf  23861  disjorf  23867  mptfnf  23917  funcnvmptOLD  23925  funcnvmpt  23926  funcnv5mpt  23927  ballotlem2  24527  axrepprim  24932  axunprim  24933  axpowprim  24934  axinfprim  24936  axacprim  24937  untuni  24939  dffr5  25136  dfon2lem8  25172  dfon2lem9  25173  19.12b  25184  predreseq  25205  dffr4  25208  brtxpsd3  25462  dfom5b  25478  dffun10  25479  elfuns  25480  mptelee  25550  heibor1lem  26211  n0el  26401  ralxpxfr2d  26434  dford4  26793  pm10.541  27233  pm10.542  27234  2exnaln  27243  19.21vv  27245  19.31vv  27253  19.28vv  27255  pm11.62  27264  ax10ext  27277  pm13.196a  27285  2sbc6g  27286  elnev  27309  conss34  27315  2rexsb  27618  2rmoswap  27632  hbexgVD  28361  bnj89  28426  bnj115  28430  bnj145  28434  bnj538  28448  bnj1143  28501  bnj110  28569  bnj611  28629  bnj864  28633  bnj865  28634  bnj1000  28652  bnj978  28660  bnj1049  28683  bnj1052  28684  bnj1090  28688  bnj1030  28696  bnj1133  28698  bnj1171  28709  bnj1172  28710  bnj1174  28712  bnj1176  28714  bnj1204  28721  bnj1253  28726  bnj1388  28742  bnj1523  28780  dvelimhwNEW7  28795  ax12olem2wAUX7  28796  equsalNEW7  28827  dvelimhvAUX7  28832  sbcomwAUX7  28925  sb8ewAUX7  28929  sbnf2NEW7  28943  2sb6NEW7  28945  sb6aNEW7  28946  sbexNEW7  28952  sbalvNEW7  28953  dvelimALTNEW7  28971  alrot3OLD7  29000  alrot4OLD7  29001  aaanOLD7  29016  pm11.53OLD7  29018  19.12vvOLD7  29019  ax12olem2OLD7  29024  dvelimhOLD7  29031  sbcomOLD7  29073  sb8eOLD7  29075  sbcom2OLD7  29079  2sb6rfOLD7  29081  2exsbOLD7  29086  sbal2OLD7  29087  pmapglbx  29885
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