Theorem albii 1516

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 1514	. 2 |- ( A. x ( ph <-> ps ) -> ( A. x ph <-> A. x ps ) )
2		albii.1	. 2 |- ( ph <-> ps )
3	1, 2	mpg 1497	1 |- ( A. x ph <-> A. x ps )

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

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 1493  ax-gen 1495

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2albii  1517  hbxfrbi  1518  nfbii  1519  19.26-2  1528  19.26-3an  1529  alrot3  1531  alrot4  1532  albiim  1533  2albiim  1534  alnex  1545  nfalt  1624  aaanh  1632  aaan  1633  alinexa  1649  exintrbi  1679  19.21-2  1713  19.31r  1727  equsalh  1772  equsal  1773  equsalv  1839  sbcof2  1856  dvelimfALT2  1863  19.23vv  1930  sbanv  1936  pm11.53  1942  nfsbxy  1993  nfsbxyt  1994  sbcomxyyz  2023  sb9  2030  sbnf2  2032  2sb6  2035  sbcom2v  2036  sb6a  2039  2sb6rf  2041  sbalyz  2050  sbal  2051  sbal1yz  2052  sbal1  2053  sbalv  2056  2exsb  2060  nfsb4t  2065  dvelimf  2066  dveeq1  2070  sbal2  2071  sb8eu  2090  sb8euh  2100  eu1  2102  eu2  2122  mo3h  2131  moanim  2152  2eu4  2171  exists1  2174  eqcom  2231  hblem  2337  abeq2  2338  abeq1  2339  nfceqi  2368  abid2f  2398  dfrex2dc  2521  ralbii2  2540  r2alf  2547  nfraldya  2565  r3al  2574  r19.21t  2605  r19.23t  2638  rabid2  2708  rabbi  2709  ralv  2817  ceqsralt  2827  gencbval  2849  rspc2gv  2919  ralab  2963  ralrab2  2968  euind  2990  reu2  2991  reu3  2993  rmo4  2996  reu8  2999  rmo3f  3000  rmoim  3004  2reuswapdc  3007  reuind  3008  2rmorex  3009  ra5  3118  rmo2ilem  3119  rmo3  3121  ssalel  3212  ss2ab  3292  ss2rab  3300  rabss  3301  uniiunlem  3313  dfdif3  3314  ddifstab  3336  ssequn1  3374  unss  3378  ralunb  3385  ssin  3426  ssddif  3438  n0rf  3504  eq0  3510  eqv  3511  rabeq0  3521  abeq0  3522  disj  3540  disj3  3544  pwss  3665  ralsnsg  3703  ralsns  3704  disjsn  3728  euabsn2  3735  snssOLD  3793  snssb  3800  snsssn  3838  dfnfc2  3905  uni0b  3912  unissb  3917  elintrab  3934  ssintrab  3945  intun  3953  intpr  3954  dfiin2g  3997  iunss  4005  dfdisj2  4060  cbvdisj  4068  disjnim  4072  dftr2  4183  dftr5  4184  trint  4196  zfnuleu  4207  vnex  4214  inex1  4217  repizf2lem  4244  axpweq  4254  zfpow  4258  axpow2  4259  axpow3  4260  exmid01  4281  zfpair2  4293  ssextss  4305  frirrg  4440  sucel  4500  zfun  4524  uniex2  4526  setindel  4629  setind  4630  elirr  4632  en2lp  4645  zfregfr  4665  tfi  4673  peano5  4689  ssrel  4806  ssrel2  4808  eqrelrel  4819  reliun  4839  raliunxp  4862  relop  4871  dmopab3  4935  dm0rn0  4939  reldm0  4940  cotr  5109  issref  5110  asymref  5113  intirr  5114  sb8iota  5285  dffun2  5327  dffun4  5328  dffun6f  5330  dffun4f  5333  dffun7  5344  funopab  5352  funcnv2  5380  funcnv  5381  funcnveq  5383  fun2cnv  5384  fun11  5387  fununi  5388  funcnvuni  5389  funimaexglem  5403  fnres  5439  fnopabg  5446  rexrnmpt  5777  dff13  5891  iotaexel  5958  oprabidlem  6031  eqoprab2b  6061  mpo2eqb  6113  ralrnmpo  6118  dfer2  6679  pw1dc0el  7069  fiintim  7089  omniwomnimkv  7330  ltexprlemdisj  7789  recexprlemdisj  7813  nnwosdc  12555  isprm2  12634  ivthdich  15321  bj-stal  16071  bj-nfalt  16086  bdceq  16163  bdcriota  16204  bj-axempty2  16215  bj-vprc  16217  bdinex1  16220  bj-zfpair2  16231  bj-uniex2  16237  bj-ssom  16257  bj-inf2vnlem2  16292  ss1oel2o  16313