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  1939  pm11.53  1945  nfsbxy  1996  nfsbxyt  1997  sbcomxyyz  2026  sb9  2033  sbnf2  2035  2sb6  2038  sbcom2v  2039  sb6a  2042  2sb6rf  2044  sbalyz  2053  sbal  2054  sbal1yz  2055  sbal1  2056  sbalv  2059  2exsb  2063  nfsb4t  2068  dvelimf  2069  dveeq1  2073  sbal2  2074  sb8eu  2093  sb8euh  2103  eu1  2105  eu2  2125  mo3h  2134  moanim  2155  2eu4  2174  exists1  2177  eqcom  2234  hblem  2340  abeq2  2341  abeq1  2342  eqabcb  2369  nfceqi  2380  abid2f  2410  dfrex2dc  2533  ralbii2  2552  r2alf  2559  nfraldya  2577  r3al  2586  r19.21t  2617  r19.23t  2650  rabid2  2720  rabbi  2721  ralv  2830  ceqsralt  2840  gencbval  2862  rspc2gv  2932  ralab  2976  ralrab2  2981  euind  3003  reu2  3004  reu3  3006  rmo4  3009  reu8  3012  rmo3f  3013  rmoim  3017  2reuswapdc  3020  reuind  3021  2rmorex  3022  ra5  3131  rmo2ilem  3132  rmo3  3134  ssalel  3225  ss2ab  3305  ss2rab  3313  rabss  3314  uniiunlem  3327  dfdif3  3328  ddifstab  3350  ssequn1  3388  unss  3392  ralunb  3399  ssin  3442  ssddif  3454  n0rf  3520  eq0  3526  eqv  3527  rabeq0  3537  abeq0  3538  disj  3556  disj3  3560  pwss  3687  ralsnsg  3725  ralsns  3726  disjsn  3750  euabsn2  3759  snssOLD  3818  snssb  3826  snsssn  3864  dfnfc2  3931  uni0b  3938  unissb  3943  elintrab  3960  ssintrab  3971  intun  3979  intpr  3980  dfiin2g  4023  iunss  4031  dfdisj2  4086  cbvdisj  4094  disjnim  4098  dftr2  4209  dftr5  4210  trint  4222  zfnuleu  4233  vnex  4240  inex1  4243  repizf2lem  4273  axpweq  4283  zfpow  4287  axpow2  4288  axpow3  4289  exmid01  4310  zfpair2  4322  ssextss  4335  frirrg  4470  sucel  4530  zfun  4554  uniex2  4556  setindel  4659  setind  4660  elirr  4662  en2lp  4675  zfregfr  4695  tfi  4703  peano5  4719  ssrel  4837  ssrel2  4839  eqrelrel  4850  reliun  4872  raliunxp  4895  relop  4904  dmopab3  4968  dm0rn0  4972  reldm0  4973  cotr  5143  issref  5144  asymref  5147  intirr  5148  sb8iota  5319  dffun2  5361  dffun4  5362  dffun6f  5364  dffun4f  5367  dffun7  5378  funopab  5386  funcnv2  5415  funcnv  5416  funcnveq  5418  fun2cnv  5419  fun11  5422  fununi  5423  funcnvuni  5424  funimaexglem  5438  fnres  5474  fnopabg  5481  rexrnmpt  5819  dff13  5940  iotaexel  6007  oprabidlem  6080  eqoprab2b  6110  mpo2eqb  6162  ralrnmpo  6167  dfer2  6767  pw1dc0el  7170  fiintim  7190  omniwomnimkv  7457  ltexprlemdisj  7920  recexprlemdisj  7944  nnwosdc  12731  isprm2  12810  ivthdich  15510  bj-stal  16513  bj-nfalt  16528  bdceq  16604  bdcriota  16645  bj-axempty2  16656  bj-vprc  16658  bdinex1  16661  bj-zfpair2  16672  bj-uniex2  16678  bj-ssom  16698  bj-inf2vnlem2  16733  ss1oel2o  16753