Theorem albii 1463

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

Syntax hints:   <-> wb 104   A.wal 1346

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  2albii  1464  hbxfrbi  1465  nfbii  1466  19.26-2  1475  19.26-3an  1476  alrot3  1478  alrot4  1479  albiim  1480  2albiim  1481  alnex  1492  nfalt  1571  aaanh  1579  aaan  1580  alinexa  1596  exintrbi  1626  19.21-2  1660  19.31r  1674  equsalh  1719  equsal  1720  equsalv  1786  sbcof2  1803  dvelimfALT2  1810  19.23vv  1877  sbanv  1882  pm11.53  1888  nfsbxy  1935  nfsbxyt  1936  sbcomxyyz  1965  sb9  1972  sbnf2  1974  2sb6  1977  sbcom2v  1978  sb6a  1981  2sb6rf  1983  sbalyz  1992  sbal  1993  sbal1yz  1994  sbal1  1995  sbalv  1998  2exsb  2002  nfsb4t  2007  dvelimf  2008  dveeq1  2012  sbal2  2013  sb8eu  2032  sb8euh  2042  eu1  2044  eu2  2063  mo3h  2072  moanim  2093  2eu4  2112  exists1  2115  eqcom  2172  hblem  2278  abeq2  2279  abeq1  2280  nfceqi  2308  abid2f  2338  dfrex2dc  2461  ralbii2  2480  r2alf  2487  nfraldya  2505  r3al  2514  r19.21t  2545  r19.23t  2577  rabid2  2646  rabbi  2647  ralv  2747  ceqsralt  2757  gencbval  2778  rspc2gv  2846  ralab  2890  ralrab2  2895  euind  2917  reu2  2918  reu3  2920  rmo4  2923  reu8  2926  rmo3f  2927  rmoim  2931  2reuswapdc  2934  reuind  2935  2rmorex  2936  ra5  3043  rmo2ilem  3044  rmo3  3046  dfss2  3136  ss2ab  3215  ss2rab  3223  rabss  3224  uniiunlem  3236  dfdif3  3237  ddifstab  3259  ssequn1  3297  unss  3301  ralunb  3308  ssin  3349  ssddif  3361  n0rf  3427  eq0  3433  eqv  3434  rabeq0  3444  abeq0  3445  disj  3463  disj3  3467  rgenm  3517  pwss  3582  ralsnsg  3620  ralsns  3621  disjsn  3645  euabsn2  3652  snss  3709  snsssn  3748  dfnfc2  3814  uni0b  3821  unissb  3826  elintrab  3843  ssintrab  3854  intun  3862  intpr  3863  dfiin2g  3906  iunss  3914  dfdisj2  3968  cbvdisj  3976  disjnim  3980  dftr2  4089  dftr5  4090  trint  4102  zfnuleu  4113  vnex  4120  inex1  4123  repizf2lem  4147  axpweq  4157  zfpow  4161  axpow2  4162  axpow3  4163  exmid01  4184  zfpair2  4195  ssextss  4205  frirrg  4335  sucel  4395  zfun  4419  uniex2  4421  setindel  4522  setind  4523  elirr  4525  en2lp  4538  zfregfr  4558  tfi  4566  peano5  4582  ssrel  4699  ssrel2  4701  eqrelrel  4712  reliun  4732  raliunxp  4752  relop  4761  dmopab3  4824  dm0rn0  4828  reldm0  4829  cotr  4992  issref  4993  asymref  4996  intirr  4997  sb8iota  5167  dffun2  5208  dffun4  5209  dffun6f  5211  dffun4f  5214  dffun7  5225  funopab  5233  funcnv2  5258  funcnv  5259  funcnveq  5261  fun2cnv  5262  fun11  5265  fununi  5266  funcnvuni  5267  funimaexglem  5281  fnres  5314  fnopabg  5321  rexrnmpt  5639  dff13  5747  oprabidlem  5884  eqoprab2b  5911  mpo2eqb  5962  ralrnmpo  5967  dfer2  6514  pw1dc0el  6889  fiintim  6906  omniwomnimkv  7143  ltexprlemdisj  7568  recexprlemdisj  7592  nnwosdc  11994  isprm2  12071  bj-stal  13784  bj-nfalt  13799  bdceq  13877  bdcriota  13918  bj-axempty2  13929  bj-vprc  13931  bdinex1  13934  bj-zfpair2  13945  bj-uniex2  13951  bj-ssom  13971  bj-inf2vnlem2  14006  ss1oel2o  14026