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  4245  axpweq  4255  zfpow  4259  axpow2  4260  axpow3  4261  exmid01  4282  zfpair2  4294  ssextss  4306  frirrg  4441  sucel  4501  zfun  4525  uniex2  4527  setindel  4630  setind  4631  elirr  4633  en2lp  4646  zfregfr  4666  tfi  4674  peano5  4690  ssrel  4807  ssrel2  4809  eqrelrel  4820  reliun  4840  raliunxp  4863  relop  4872  dmopab3  4936  dm0rn0  4940  reldm0  4941  cotr  5110  issref  5111  asymref  5114  intirr  5115  sb8iota  5286  dffun2  5328  dffun4  5329  dffun6f  5331  dffun4f  5334  dffun7  5345  funopab  5353  funcnv2  5381  funcnv  5382  funcnveq  5384  fun2cnv  5385  fun11  5388  fununi  5389  funcnvuni  5390  funimaexglem  5404  fnres  5440  fnopabg  5447  rexrnmpt  5780  dff13  5898  iotaexel  5965  oprabidlem  6038  eqoprab2b  6068  mpo2eqb  6120  ralrnmpo  6125  dfer2  6689  pw1dc0el  7081  fiintim  7101  omniwomnimkv  7342  ltexprlemdisj  7801  recexprlemdisj  7825  nnwosdc  12568  isprm2  12647  ivthdich  15335  bj-stal  16137  bj-nfalt  16152  bdceq  16229  bdcriota  16270  bj-axempty2  16281  bj-vprc  16283  bdinex1  16286  bj-zfpair2  16297  bj-uniex2  16303  bj-ssom  16323  bj-inf2vnlem2  16358  ss1oel2o  16380