Theorem albii 1494

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

Syntax hints:   ↔ wb 105  ∀wal 1371

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 1471  ax-gen 1473

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2albii  1495  hbxfrbi  1496  nfbii  1497  19.26-2  1506  19.26-3an  1507  alrot3  1509  alrot4  1510  albiim  1511  2albiim  1512  alnex  1523  nfalt  1602  aaanh  1610  aaan  1611  alinexa  1627  exintrbi  1657  19.21-2  1691  19.31r  1705  equsalh  1750  equsal  1751  equsalv  1817  sbcof2  1834  dvelimfALT2  1841  19.23vv  1908  sbanv  1914  pm11.53  1920  nfsbxy  1971  nfsbxyt  1972  sbcomxyyz  2001  sb9  2008  sbnf2  2010  2sb6  2013  sbcom2v  2014  sb6a  2017  2sb6rf  2019  sbalyz  2028  sbal  2029  sbal1yz  2030  sbal1  2031  sbalv  2034  2exsb  2038  nfsb4t  2043  dvelimf  2044  dveeq1  2048  sbal2  2049  sb8eu  2068  sb8euh  2078  eu1  2080  eu2  2099  mo3h  2108  moanim  2129  2eu4  2148  exists1  2151  eqcom  2208  hblem  2314  abeq2  2315  abeq1  2316  nfceqi  2345  abid2f  2375  dfrex2dc  2498  ralbii2  2517  r2alf  2524  nfraldya  2542  r3al  2551  r19.21t  2582  r19.23t  2614  rabid2  2684  rabbi  2685  ralv  2791  ceqsralt  2801  gencbval  2823  rspc2gv  2891  ralab  2935  ralrab2  2940  euind  2962  reu2  2963  reu3  2965  rmo4  2968  reu8  2971  rmo3f  2972  rmoim  2976  2reuswapdc  2979  reuind  2980  2rmorex  2981  ra5  3089  rmo2ilem  3090  rmo3  3092  ssalel  3183  ss2ab  3263  ss2rab  3271  rabss  3272  uniiunlem  3284  dfdif3  3285  ddifstab  3307  ssequn1  3345  unss  3349  ralunb  3356  ssin  3397  ssddif  3409  n0rf  3475  eq0  3481  eqv  3482  rabeq0  3492  abeq0  3493  disj  3511  disj3  3515  pwss  3634  ralsnsg  3672  ralsns  3673  disjsn  3697  euabsn2  3704  snssOLD  3762  snssb  3769  snsssn  3805  dfnfc2  3871  uni0b  3878  unissb  3883  elintrab  3900  ssintrab  3911  intun  3919  intpr  3920  dfiin2g  3963  iunss  3971  dfdisj2  4026  cbvdisj  4034  disjnim  4038  dftr2  4149  dftr5  4150  trint  4162  zfnuleu  4173  vnex  4180  inex1  4183  repizf2lem  4210  axpweq  4220  zfpow  4224  axpow2  4225  axpow3  4226  exmid01  4247  zfpair2  4259  ssextss  4269  frirrg  4402  sucel  4462  zfun  4486  uniex2  4488  setindel  4591  setind  4592  elirr  4594  en2lp  4607  zfregfr  4627  tfi  4635  peano5  4651  ssrel  4768  ssrel2  4770  eqrelrel  4781  reliun  4801  raliunxp  4824  relop  4833  dmopab3  4897  dm0rn0  4901  reldm0  4902  cotr  5070  issref  5071  asymref  5074  intirr  5075  sb8iota  5245  dffun2  5287  dffun4  5288  dffun6f  5290  dffun4f  5293  dffun7  5304  funopab  5312  funcnv2  5340  funcnv  5341  funcnveq  5343  fun2cnv  5344  fun11  5347  fununi  5348  funcnvuni  5349  funimaexglem  5363  fnres  5399  fnopabg  5406  rexrnmpt  5733  dff13  5847  iotaexel  5914  oprabidlem  5985  eqoprab2b  6013  mpo2eqb  6065  ralrnmpo  6070  dfer2  6631  pw1dc0el  7020  fiintim  7040  omniwomnimkv  7281  ltexprlemdisj  7732  recexprlemdisj  7756  nnwosdc  12410  isprm2  12489  ivthdich  15175  bj-stal  15799  bj-nfalt  15814  bdceq  15892  bdcriota  15933  bj-axempty2  15944  bj-vprc  15946  bdinex1  15949  bj-zfpair2  15960  bj-uniex2  15966  bj-ssom  15986  bj-inf2vnlem2  16021  ss1oel2o  16042