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	⊢ (𝜑 ↔ 𝜓)

Assertion

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

Proof of Theorem albii

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

Syntax hints:   ↔ wb 105  ∀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  3794  snssb  3801  snsssn  3839  dfnfc2  3906  uni0b  3913  unissb  3918  elintrab  3935  ssintrab  3946  intun  3954  intpr  3955  dfiin2g  3998  iunss  4006  dfdisj2  4061  cbvdisj  4069  disjnim  4073  dftr2  4184  dftr5  4185  trint  4197  zfnuleu  4208  vnex  4215  inex1  4218  repizf2lem  4246  axpweq  4256  zfpow  4260  axpow2  4261  axpow3  4262  exmid01  4283  zfpair2  4295  ssextss  4307  frirrg  4442  sucel  4502  zfun  4526  uniex2  4528  setindel  4631  setind  4632  elirr  4634  en2lp  4647  zfregfr  4667  tfi  4675  peano5  4691  ssrel  4809  ssrel2  4811  eqrelrel  4822  reliun  4843  raliunxp  4866  relop  4875  dmopab3  4939  dm0rn0  4943  reldm0  4944  cotr  5113  issref  5114  asymref  5117  intirr  5118  sb8iota  5289  dffun2  5331  dffun4  5332  dffun6f  5334  dffun4f  5337  dffun7  5348  funopab  5356  funcnv2  5384  funcnv  5385  funcnveq  5387  fun2cnv  5388  fun11  5391  fununi  5392  funcnvuni  5393  funimaexglem  5407  fnres  5443  fnopabg  5450  rexrnmpt  5783  dff13  5901  iotaexel  5968  oprabidlem  6041  eqoprab2b  6071  mpo2eqb  6123  ralrnmpo  6128  dfer2  6694  pw1dc0el  7089  fiintim  7109  omniwomnimkv  7350  ltexprlemdisj  7809  recexprlemdisj  7833  nnwosdc  12581  isprm2  12660  ivthdich  15348  bj-stal  16222  bj-nfalt  16237  bdceq  16314  bdcriota  16355  bj-axempty2  16366  bj-vprc  16368  bdinex1  16371  bj-zfpair2  16382  bj-uniex2  16388  bj-ssom  16408  bj-inf2vnlem2  16443  ss1oel2o  16464