Theorem albii 1427

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

Syntax hints:   ↔ wb 104  ∀wal 1310

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-gen 1406

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  2albii  1428  hbxfrbi  1429  nfbii  1430  19.26-2  1439  19.26-3an  1440  alrot3  1442  alrot4  1443  albiim  1444  2albiim  1445  alnex  1456  nfalt  1538  aaanh  1546  aaan  1547  alinexa  1563  exintrbi  1593  19.21-2  1626  19.31r  1640  equsalh  1685  equsal  1686  sbcof2  1762  dvelimfALT2  1769  19.23vv  1836  sbanv  1841  pm11.53  1847  nfsbxy  1891  nfsbxyt  1892  sbcomxyyz  1919  sb9  1928  sbnf2  1930  2sb6  1933  sbcom2v  1934  sb6a  1937  2sb6rf  1939  sbalyz  1948  sbal  1949  sbal1yz  1950  sbal1  1951  sbalv  1954  2exsb  1958  nfsb4t  1963  dvelimf  1964  dveeq1  1968  sbal2  1971  sb8eu  1986  sb8euh  1996  eu1  1998  eu2  2017  mo3h  2026  moanim  2047  2eu4  2066  exists1  2069  eqcom  2115  hblem  2220  abeq2  2221  abeq1  2222  nfceqi  2249  abid2f  2278  dfrex2dc  2400  ralbii2  2417  r2alf  2424  nfraldya  2441  r3al  2449  r19.21t  2479  r19.23t  2511  rabid2  2579  rabbi  2580  ralv  2672  ceqsralt  2682  gencbval  2703  rspc2gv  2769  ralab  2811  ralrab2  2816  euind  2838  reu2  2839  reu3  2841  rmo4  2844  reu8  2847  rmo3f  2848  rmoim  2852  2reuswapdc  2855  reuind  2856  2rmorex  2857  ra5  2963  rmo2ilem  2964  rmo3  2966  dfss2  3050  ss2ab  3129  ss2rab  3137  rabss  3138  uniiunlem  3149  dfdif3  3150  ddifstab  3172  ssequn1  3210  unss  3214  ralunb  3221  ssin  3262  ssddif  3274  n0rf  3339  eq0  3345  eqv  3346  rabeq0  3356  abeq0  3357  disj  3375  disj3  3379  rgenm  3429  pwss  3490  ralsnsg  3525  ralsns  3526  disjsn  3549  euabsn2  3556  snss  3613  snsssn  3652  dfnfc2  3718  uni0b  3725  unissb  3730  elintrab  3747  ssintrab  3758  intun  3766  intpr  3767  dfiin2g  3810  iunss  3818  dfdisj2  3872  cbvdisj  3880  disjnim  3884  dftr2  3986  dftr5  3987  trint  3999  zfnuleu  4010  vnex  4017  inex1  4020  repizf2lem  4043  axpweq  4053  zfpow  4057  axpow2  4058  axpow3  4059  exmid01  4079  zfpair2  4090  ssextss  4100  frirrg  4230  sucel  4290  zfun  4314  uniex2  4316  setindel  4411  setind  4412  elirr  4414  en2lp  4427  zfregfr  4446  tfi  4454  peano5  4470  ssrel  4585  ssrel2  4587  eqrelrel  4598  reliun  4618  raliunxp  4638  relop  4647  dmopab3  4710  dm0rn0  4714  reldm0  4715  cotr  4876  issref  4877  asymref  4880  intirr  4881  sb8iota  5051  dffun2  5089  dffun4  5090  dffun6f  5092  dffun4f  5095  dffun7  5106  funopab  5114  funcnv2  5139  funcnv  5140  funcnveq  5142  fun2cnv  5143  fun11  5146  fununi  5147  funcnvuni  5148  funimaexglem  5162  fnres  5195  fnopabg  5202  rexrnmpt  5515  dff13  5621  oprabidlem  5754  eqoprab2b  5781  mpo2eqb  5832  ralrnmpo  5837  dfer2  6381  fiintim  6767  ltexprlemdisj  7355  recexprlemdisj  7379  isprm2  11637  bj-stal  12636  bj-nfalt  12651  bdceq  12719  bdcriota  12760  bj-axempty2  12771  bj-vprc  12773  bdinex1  12776  bj-zfpair2  12787  bj-uniex2  12793  bj-ssom  12813  bj-inf2vnlem2  12848  ss1oel2o  12868