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  1841  sbcof2  1858  dvelimfALT2  1865  19.23vv  1932  sbanv  1938  pm11.53  1944  nfsbxy  1995  nfsbxyt  1996  sbcomxyyz  2025  sb9  2032  sbnf2  2034  2sb6  2037  sbcom2v  2038  sb6a  2041  2sb6rf  2043  sbalyz  2052  sbal  2053  sbal1yz  2054  sbal1  2055  sbalv  2058  2exsb  2062  nfsb4t  2067  dvelimf  2068  dveeq1  2072  sbal2  2073  sb8eu  2092  sb8euh  2102  eu1  2104  eu2  2124  mo3h  2133  moanim  2154  2eu4  2173  exists1  2176  eqcom  2233  hblem  2339  abeq2  2340  abeq1  2341  nfceqi  2371  abid2f  2401  dfrex2dc  2524  ralbii2  2543  r2alf  2550  nfraldya  2568  r3al  2577  r19.21t  2608  r19.23t  2641  rabid2  2711  rabbi  2712  ralv  2821  ceqsralt  2831  gencbval  2853  rspc2gv  2923  ralab  2967  ralrab2  2972  euind  2994  reu2  2995  reu3  2997  rmo4  3000  reu8  3003  rmo3f  3004  rmoim  3008  2reuswapdc  3011  reuind  3012  2rmorex  3013  ra5  3122  rmo2ilem  3123  rmo3  3125  ssalel  3216  ss2ab  3296  ss2rab  3304  rabss  3305  uniiunlem  3318  dfdif3  3319  ddifstab  3341  ssequn1  3379  unss  3383  ralunb  3390  ssin  3431  ssddif  3443  n0rf  3509  eq0  3515  eqv  3516  rabeq0  3526  abeq0  3527  disj  3545  disj3  3549  pwss  3672  ralsnsg  3710  ralsns  3711  disjsn  3735  euabsn2  3744  snssOLD  3803  snssb  3811  snsssn  3849  dfnfc2  3916  uni0b  3923  unissb  3928  elintrab  3945  ssintrab  3956  intun  3964  intpr  3965  dfiin2g  4008  iunss  4016  dfdisj2  4071  cbvdisj  4079  disjnim  4083  dftr2  4194  dftr5  4195  trint  4207  zfnuleu  4218  vnex  4225  inex1  4228  repizf2lem  4257  axpweq  4267  zfpow  4271  axpow2  4272  axpow3  4273  exmid01  4294  zfpair2  4306  ssextss  4318  frirrg  4453  sucel  4513  zfun  4537  uniex2  4539  setindel  4642  setind  4643  elirr  4645  en2lp  4658  zfregfr  4678  tfi  4686  peano5  4702  ssrel  4820  ssrel2  4822  eqrelrel  4833  reliun  4854  raliunxp  4877  relop  4886  dmopab3  4950  dm0rn0  4954  reldm0  4955  cotr  5125  issref  5126  asymref  5129  intirr  5130  sb8iota  5301  dffun2  5343  dffun4  5344  dffun6f  5346  dffun4f  5349  dffun7  5360  funopab  5368  funcnv2  5397  funcnv  5398  funcnveq  5400  fun2cnv  5401  fun11  5404  fununi  5405  funcnvuni  5406  funimaexglem  5420  fnres  5456  fnopabg  5463  rexrnmpt  5798  dff13  5919  iotaexel  5986  oprabidlem  6059  eqoprab2b  6089  mpo2eqb  6141  ralrnmpo  6146  dfer2  6746  pw1dc0el  7146  fiintim  7166  omniwomnimkv  7409  ltexprlemdisj  7869  recexprlemdisj  7893  nnwosdc  12671  isprm2  12750  ivthdich  15444  bj-stal  16447  bj-nfalt  16462  bdceq  16538  bdcriota  16579  bj-axempty2  16590  bj-vprc  16592  bdinex1  16595  bj-zfpair2  16606  bj-uniex2  16612  bj-ssom  16632  bj-inf2vnlem2  16667  ss1oel2o  16687