Theorem albii 1566

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.xph <-> A.xps)

Proof of Theorem albii

Step	Hyp	Ref	Expression
1		albi 1564	. 2 |- (A.x(ph <-> ps) -> (A.xph <-> A.xps))
2		albii.1	. 2 |- (ph <-> ps)
3	1, 2	mpg 1548	1 |- (A.xph <-> A.xps)

Syntax hints:   <-> wb 176  A.wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  2albii  1567  hbxfrbi  1568  nfbii  1569  alex  1572  2nalexn  1573  alinexa  1578  alexn  1579  19.26-2  1594  19.26-3an  1595  19.35  1600  19.30  1604  19.43OLD  1606  albiim  1611  2albiim  1612  exintrbi  1613  19.8wOLD  1693  alrot3  1738  alrot4  1739  hba1  1786  equsalhw  1838  equsalhwOLD  1839  dvelimhw  1849  19.21-2  1864  19.32  1875  19.31  1876  aaan  1884  19.23vv  1892  pm11.53  1893  19.12vv  1898  ax12olem2  1928  equsal  1960  dvelimh  1964  sbcom  2089  sb8e  2093  sbnf2  2108  2sb6  2113  sbcom2  2114  sb6a  2116  2sb6rf  2118  sbex  2128  sbalv  2129  2exsb  2132  dvelimALT  2133  sbal2  2134  dvelimf-o  2180  ax10-16  2190  sb8eu  2222  eu1  2225  eu2  2229  moanim  2260  2mo  2282  2eu3  2286  2eu4  2287  exists1  2293  eqcom  2355  hblem  2458  abeq2  2459  abeq1  2460  nfceqi  2486  abid2f  2515  ralbii2  2643  r2alf  2650  r3al  2672  r19.21t  2700  r19.23t  2729  rabid2  2789  rabbi  2790  ralv  2873  ceqsralt  2883  ralab  2998  ralrab2  3003  euind  3024  reu2  3025  reu3  3027  rmo4  3030  reu8  3033  rmoim  3036  2reuswap  3039  reuind  3040  2reu5lem2  3043  2reu5lem3  3044  ra5  3131  rmo2  3132  rmo3  3134  dfss2  3263  ss2ab  3335  ss2rab  3343  rabss  3344  uniiunlem  3354  ssequn1  3434  unss  3438  ralunb  3445  ssin  3478  n0f  3559  eqv  3566  disj  3592  disj3  3596  ssdif0  3610  inssdif0  3618  ssundif  3634  sscon34  3662  pwss  3737  ralsns  3764  disjsn  3787  euabsn2  3792  snss  3839  pwpw0  3856  pwsnALT  3883  dfnfc2  3910  unissb  3922  elintrab  3939  ssintrab  3950  intun  3959  intpr  3960  dfiin2g  4001  iunss  4008  axprimlem1  4089  axprimlem2  4090  axxpprim  4091  axsiprim  4094  axtyplowerprim  4095  axins2prim  4096  axins3prim  4097  ninexg  4098  1cex  4143  eqpw1  4163  pw111  4171  ssrelk  4212  eqrelk  4213  elp6  4264  xpkvexg  4286  p6exg  4291  dfuni12  4292  sikexlem  4296  dfimak2  4299  insklem  4305  ins2kexg  4306  ins3kexg  4307  sb8iota  4347  ssfin  4471  nnadjoin  4521  nnadjoinpw  4522  nnpweq  4524  tfinnn  4535  spfininduct  4541  eqop  4612  raliunxp  4824  ssopr  4847  eqopr  4848  dmopab3  4918  dm0rn0  4922  dmeq0  4923  cotr  5027  intirr  5030  dffun3  5121  dffun4  5122  dffun5  5123  dffun6f  5124  dffun7  5134  funopab  5140  funcnv2  5156  funcnv  5157  fun11  5160  fununi  5161  funcnvuni  5162  fnres  5200  fnopabg  5206  dff13  5472  fvfullfunlem1  5862  clos1induct  5881  dfnnc3  5886  frds  5936  enmap2lem4  6067  enmap1lem4  6073  ncssfin  6152  spacind  6288