Theorem albii 1518

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

Step	Hyp	Ref	Expression
1		albi 1516	. 2 |- ( A. x ( ph <-> ps ) -> ( A. x ph <-> A. x ps ) )
2		albii.1	. 2 |- ( ph <-> ps )
3	1, 2	mpg 1499	1 |- ( A. x ph <-> A. x ps )

Syntax hints:   <-> wb 105   A.wal 1395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2albii  1519  hbxfrbi  1520  nfbii  1521  19.26-2  1530  19.26-3an  1531  alrot3  1533  alrot4  1534  albiim  1535  2albiim  1536  alnex  1547  nfalt  1626  aaanh  1634  aaan  1635  alinexa  1651  exintrbi  1681  19.21-2  1715  19.31r  1729  equsalh  1774  equsal  1775  equsalv  1841  sbcof2  1858  dvelimfALT2  1865  19.23vv  1932  sbanv  1938  pm11.53  1944  nfsbxy  1995  nfsbxyt  1996  sbcomxyyz  2025  sb9  2032  sbnf2  2034  2sb6  2037  sbcom2v  2038  sb6a  2041  2sb6rf  2043  sbalyz  2052  sbal  2053  sbal1yz  2054  sbal1  2055  sbalv  2058  2exsb  2062  nfsb4t  2067  dvelimf  2068  dveeq1  2072  sbal2  2073  sb8eu  2092  sb8euh  2102  eu1  2104  eu2  2124  mo3h  2133  moanim  2154  2eu4  2173  exists1  2176  eqcom  2233  hblem  2339  abeq2  2340  abeq1  2341  nfceqi  2370  abid2f  2400  dfrex2dc  2523  ralbii2  2542  r2alf  2549  nfraldya  2567  r3al  2576  r19.21t  2607  r19.23t  2640  rabid2  2710  rabbi  2711  ralv  2820  ceqsralt  2830  gencbval  2852  rspc2gv  2922  ralab  2966  ralrab2  2971  euind  2993  reu2  2994  reu3  2996  rmo4  2999  reu8  3002  rmo3f  3003  rmoim  3007  2reuswapdc  3010  reuind  3011  2rmorex  3012  ra5  3121  rmo2ilem  3122  rmo3  3124  ssalel  3215  ss2ab  3295  ss2rab  3303  rabss  3304  uniiunlem  3316  dfdif3  3317  ddifstab  3339  ssequn1  3377  unss  3381  ralunb  3388  ssin  3429  ssddif  3441  n0rf  3507  eq0  3513  eqv  3514  rabeq0  3524  abeq0  3525  disj  3543  disj3  3547  pwss  3668  ralsnsg  3706  ralsns  3707  disjsn  3731  euabsn2  3740  snssOLD  3799  snssb  3806  snsssn  3844  dfnfc2  3911  uni0b  3918  unissb  3923  elintrab  3940  ssintrab  3951  intun  3959  intpr  3960  dfiin2g  4003  iunss  4011  dfdisj2  4066  cbvdisj  4074  disjnim  4078  dftr2  4189  dftr5  4190  trint  4202  zfnuleu  4213  vnex  4220  inex1  4223  repizf2lem  4251  axpweq  4261  zfpow  4265  axpow2  4266  axpow3  4267  exmid01  4288  zfpair2  4300  ssextss  4312  frirrg  4447  sucel  4507  zfun  4531  uniex2  4533  setindel  4636  setind  4637  elirr  4639  en2lp  4652  zfregfr  4672  tfi  4680  peano5  4696  ssrel  4814  ssrel2  4816  eqrelrel  4827  reliun  4848  raliunxp  4871  relop  4880  dmopab3  4944  dm0rn0  4948  reldm0  4949  cotr  5118  issref  5119  asymref  5122  intirr  5123  sb8iota  5294  dffun2  5336  dffun4  5337  dffun6f  5339  dffun4f  5342  dffun7  5353  funopab  5361  funcnv2  5390  funcnv  5391  funcnveq  5393  fun2cnv  5394  fun11  5397  fununi  5398  funcnvuni  5399  funimaexglem  5413  fnres  5449  fnopabg  5456  rexrnmpt  5790  dff13  5908  iotaexel  5975  oprabidlem  6048  eqoprab2b  6078  mpo2eqb  6130  ralrnmpo  6135  dfer2  6702  pw1dc0el  7102  fiintim  7122  omniwomnimkv  7365  ltexprlemdisj  7825  recexprlemdisj  7849  nnwosdc  12609  isprm2  12688  ivthdich  15376  bj-stal  16345  bj-nfalt  16360  bdceq  16437  bdcriota  16478  bj-axempty2  16489  bj-vprc  16491  bdinex1  16494  bj-zfpair2  16505  bj-uniex2  16511  bj-ssom  16531  bj-inf2vnlem2  16566  ss1oel2o  16586