Theorem albii 1519

Description: Inference adding universal quantifier to both sides of an equivalence. (Contributed by NM, 7-Aug-1994.)

Hypothesis

Ref	Expression
albii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
albii	⊢ (∀𝑥𝜑 ↔ ∀𝑥𝜓)

Proof of Theorem albii

Step	Hyp	Ref	Expression
1		albi 1517	. 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∀𝑥𝜑 ↔ ∀𝑥𝜓))
2		albii.1	. 2 ⊢ (𝜑 ↔ 𝜓)
3	1, 2	mpg 1500	1 ⊢ (∀𝑥𝜑 ↔ ∀𝑥𝜓)

Syntax hints:   ↔ wb 105  ∀wal 1396

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 1496  ax-gen 1498

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2albii  1520  hbxfrbi  1521  nfbii  1522  19.26-2  1531  19.26-3an  1532  alrot3  1534  alrot4  1535  albiim  1536  2albiim  1537  alnex  1548  nfalt  1627  aaanh  1635  aaan  1636  alinexa  1652  exintrbi  1682  19.21-2  1715  19.31r  1729  equsalh  1774  equsal  1775  equsalv  1842  sbcof2  1859  dvelimfALT2  1866  19.23vv  1933  sbanv  1940  pm11.53  1947  nfsbxy  1998  nfsbxyt  1999  sbcomxyyz  2028  sb9  2035  sbnf2  2037  2sb6  2040  sbcom2v  2041  sb6a  2044  2sb6rf  2046  sbalyz  2055  sbal  2056  sbal1yz  2057  sbal1  2058  sbalv  2061  2exsb  2065  nfsb4t  2070  dvelimf  2071  dveeq1  2075  sbal2  2076  sb8eu  2095  sb8euh  2105  eu1  2107  eu2  2127  mo3h  2136  moanim  2157  2eu4  2176  exists1  2179  eqcom  2236  hblem  2342  abeq2  2343  abeq1  2344  eqabcb  2371  nfceqi  2382  abid2f  2412  dfrex2dc  2535  ralbii2  2554  r2alf  2561  nfraldya  2579  r3al  2588  r19.21t  2619  r19.23t  2652  rabid2  2723  rabbi  2724  ralv  2833  ceqsralt  2843  gencbval  2865  rspc2gv  2936  ralab  2980  ralrab2  2985  euind  3007  reu2  3008  reu3  3010  rmo4  3013  reu8  3016  rmo3f  3017  rmoim  3021  2reuswapdc  3024  reuind  3025  2rmorex  3026  ra5  3135  rmo2ilem  3136  rmo3  3138  ssalel  3229  ss2ab  3310  ss2rab  3318  rabss  3319  uniiunlem  3332  dfdif3  3333  ddifstab  3355  ssequn1  3393  unss  3397  ralunb  3404  ssin  3447  ssddif  3459  n0rf  3525  eq0  3531  eqv  3532  rabeq0  3542  abeq0  3543  disj  3561  disj3  3565  pwss  3693  ralsnsg  3731  ralsns  3732  disjsn  3756  euabsn2  3765  snssOLD  3824  snssb  3832  snsssn  3870  dfnfc2  3937  uni0b  3944  unissb  3949  elintrab  3966  ssintrab  3977  intun  3985  intpr  3986  dfiin2g  4029  iunss  4037  dfdisj2  4092  cbvdisj  4100  disjnim  4104  dftr2  4215  dftr5  4216  trint  4228  zfnuleu  4239  vnex  4246  inex1  4249  repizf2lem  4279  axpweq  4289  zfpow  4293  axpow2  4294  axpow3  4295  exmid01  4316  zfpair2  4328  ssextss  4341  frirrg  4476  sucel  4536  zfun  4560  uniex2  4562  setindel  4665  setind  4666  elirr  4668  en2lp  4681  zfregfr  4701  tfi  4709  peano5  4725  ssrel  4843  ssrel2  4845  eqrelrel  4856  reliun  4878  raliunxp  4901  relop  4910  dmopab3  4974  dm0rn0  4978  reldm0  4979  cotr  5149  issref  5150  asymref  5153  intirr  5154  sb8iota  5325  dffun2  5367  dffun4  5368  dffun6f  5370  dffun4f  5373  dffun7  5384  funopab  5392  funcnv2  5421  funcnv  5422  funcnveq  5424  fun2cnv  5425  fun11  5428  fununi  5429  funcnvuni  5430  funimaexglem  5444  fnres  5480  fnopabg  5487  rexrnmpt  5825  dff13  5947  iotaexel  6016  oprabidlem  6089  eqoprab2b  6119  mpo2eqb  6171  ralrnmpo  6176  dfer2  6781  pw1dc0el  7184  fiintim  7204  omniwomnimkv  7471  ltexprlemdisj  7937  recexprlemdisj  7961  nnwosdc  12760  isprm2  12839  ivthdich  15630  bj-stal  16633  bj-nfalt  16648  bdceq  16724  bdcriota  16765  bj-axempty2  16776  bj-vprc  16778  bdinex1  16781  bj-zfpair2  16792  bj-uniex2  16798  bj-ssom  16818  bj-inf2vnlem2  16853  ss1oel2o  16873