Theorem albii 1484

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 1482	. 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∀𝑥𝜑 ↔ ∀𝑥𝜓))
2		albii.1	. 2 ⊢ (𝜑 ↔ 𝜓)
3	1, 2	mpg 1465	1 ⊢ (∀𝑥𝜑 ↔ ∀𝑥𝜓)

Syntax hints:   ↔ wb 105  ∀wal 1362

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 1461  ax-gen 1463

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2albii  1485  hbxfrbi  1486  nfbii  1487  19.26-2  1496  19.26-3an  1497  alrot3  1499  alrot4  1500  albiim  1501  2albiim  1502  alnex  1513  nfalt  1592  aaanh  1600  aaan  1601  alinexa  1617  exintrbi  1647  19.21-2  1681  19.31r  1695  equsalh  1740  equsal  1741  equsalv  1807  sbcof2  1824  dvelimfALT2  1831  19.23vv  1898  sbanv  1904  pm11.53  1910  nfsbxy  1961  nfsbxyt  1962  sbcomxyyz  1991  sb9  1998  sbnf2  2000  2sb6  2003  sbcom2v  2004  sb6a  2007  2sb6rf  2009  sbalyz  2018  sbal  2019  sbal1yz  2020  sbal1  2021  sbalv  2024  2exsb  2028  nfsb4t  2033  dvelimf  2034  dveeq1  2038  sbal2  2039  sb8eu  2058  sb8euh  2068  eu1  2070  eu2  2089  mo3h  2098  moanim  2119  2eu4  2138  exists1  2141  eqcom  2198  hblem  2304  abeq2  2305  abeq1  2306  nfceqi  2335  abid2f  2365  dfrex2dc  2488  ralbii2  2507  r2alf  2514  nfraldya  2532  r3al  2541  r19.21t  2572  r19.23t  2604  rabid2  2674  rabbi  2675  ralv  2780  ceqsralt  2790  gencbval  2812  rspc2gv  2880  ralab  2924  ralrab2  2929  euind  2951  reu2  2952  reu3  2954  rmo4  2957  reu8  2960  rmo3f  2961  rmoim  2965  2reuswapdc  2968  reuind  2969  2rmorex  2970  ra5  3078  rmo2ilem  3079  rmo3  3081  ssalel  3172  ss2ab  3252  ss2rab  3260  rabss  3261  uniiunlem  3273  dfdif3  3274  ddifstab  3296  ssequn1  3334  unss  3338  ralunb  3345  ssin  3386  ssddif  3398  n0rf  3464  eq0  3470  eqv  3471  rabeq0  3481  abeq0  3482  disj  3500  disj3  3504  pwss  3622  ralsnsg  3660  ralsns  3661  disjsn  3685  euabsn2  3692  snssOLD  3749  snssb  3756  snsssn  3792  dfnfc2  3858  uni0b  3865  unissb  3870  elintrab  3887  ssintrab  3898  intun  3906  intpr  3907  dfiin2g  3950  iunss  3958  dfdisj2  4013  cbvdisj  4021  disjnim  4025  dftr2  4134  dftr5  4135  trint  4147  zfnuleu  4158  vnex  4165  inex1  4168  repizf2lem  4195  axpweq  4205  zfpow  4209  axpow2  4210  axpow3  4211  exmid01  4232  zfpair2  4244  ssextss  4254  frirrg  4386  sucel  4446  zfun  4470  uniex2  4472  setindel  4575  setind  4576  elirr  4578  en2lp  4591  zfregfr  4611  tfi  4619  peano5  4635  ssrel  4752  ssrel2  4754  eqrelrel  4765  reliun  4785  raliunxp  4808  relop  4817  dmopab3  4880  dm0rn0  4884  reldm0  4885  cotr  5052  issref  5053  asymref  5056  intirr  5057  sb8iota  5227  dffun2  5269  dffun4  5270  dffun6f  5272  dffun4f  5275  dffun7  5286  funopab  5294  funcnv2  5319  funcnv  5320  funcnveq  5322  fun2cnv  5323  fun11  5326  fununi  5327  funcnvuni  5328  funimaexglem  5342  fnres  5377  fnopabg  5384  rexrnmpt  5708  dff13  5818  iotaexel  5885  oprabidlem  5956  eqoprab2b  5984  mpo2eqb  6036  ralrnmpo  6041  dfer2  6602  pw1dc0el  6981  fiintim  7001  omniwomnimkv  7242  ltexprlemdisj  7690  recexprlemdisj  7714  nnwosdc  12231  isprm2  12310  ivthdich  14973  bj-stal  15479  bj-nfalt  15494  bdceq  15572  bdcriota  15613  bj-axempty2  15624  bj-vprc  15626  bdinex1  15629  bj-zfpair2  15640  bj-uniex2  15646  bj-ssom  15666  bj-inf2vnlem2  15701  ss1oel2o  15722