Theorem albii 1523

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

Syntax hints:   ↔ wb 105  ∀wal 1400

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 1500  ax-gen 1502

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2albii  1524  hbxfrbi  1525  nfbii  1526  19.26-2  1535  19.26-3an  1536  alrot3  1538  alrot4  1539  albiim  1540  2albiim  1541  alnex  1552  nfalt  1631  aaanh  1639  aaan  1640  alinexa  1656  exintrbi  1686  19.21-2  1719  19.31r  1733  equsalh  1778  equsal  1779  equsalv  1846  sbcof2  1863  dvelimfALT2  1870  19.23vv  1937  sbanv  1944  pm11.53  1951  nfsbxy  2002  nfsbxyt  2003  sbcomxyyz  2032  sb9  2039  sbnf2  2041  2sb6  2044  sbcom2v  2045  sb6a  2048  2sb6rf  2050  sbalyz  2059  sbal  2060  sbal1yz  2061  sbal1  2062  sbalv  2065  2exsb  2069  nfsb4t  2074  dvelimf  2075  dveeq1  2079  sbal2  2080  sb8eu  2099  sb8euh  2109  eu1  2111  eu2  2131  mo3h  2140  moanim  2161  2eu4  2180  exists1  2183  eqcom  2240  hblem  2346  abeq2  2347  abeq1  2348  eqabcbw  2376  eqabcb  2377  nfceqi  2388  abid2f  2418  dfrex2dc  2541  ralbii2  2560  r2alf  2567  nfraldya  2585  r3al  2594  r19.21t  2625  r19.23t  2658  rabid2  2729  rabbi  2730  ralv  2839  ceqsralt  2849  gencbval  2871  rspc2gv  2942  ralab  2986  ralrab2  2991  euind  3013  reu2  3014  reu3  3016  rmo4  3019  reu8  3022  rmo3f  3023  rmoim  3027  2reuswapdc  3030  reuind  3031  2rmorex  3032  ra5  3141  rmo2ilem  3142  rmo3  3144  ssalel  3235  ss2ab  3316  ss2rab  3324  rabss  3325  uniiunlem  3338  dfdif3  3339  ddifstab  3361  ssequn1  3399  unss  3403  ralunb  3410  ssin  3453  ssddif  3465  n0rf  3534  eq0  3540  eqv  3541  ab0w  3550  rabeq0  3552  abeq0  3553  disj  3573  disj3  3577  pwss  3707  ralsnsg  3745  ralsns  3746  disjsn  3770  euabsn2  3779  snssOLD  3838  snssb  3846  snsssn  3884  dfnfc2  3951  uni0b  3958  unissb  3963  elintrab  3980  ssintrab  3991  intun  3999  intpr  4000  dfiin2g  4043  iunss  4051  dfdisj2  4106  cbvdisj  4114  disjnim  4118  dftr2  4229  dftr5  4230  trint  4242  zfnuleu  4255  vnex  4262  inex1  4265  repizf2lem  4296  axpweq  4306  zfpow  4310  axpow2  4311  axpow3  4312  exmid01  4333  zfpair2  4345  ssextss  4358  frirrg  4493  sucel  4553  zfun  4577  uniex2  4579  uniex2OLD  4580  setindel  4683  setind  4684  elirr  4686  en2lp  4699  zfregfr  4719  tfi  4727  peano5  4743  ssrel  4861  ssrel2  4863  eqrelrel  4874  reliun  4896  raliunxp  4919  relop  4928  dmopab3  4992  dm0rn0  4996  reldm0  4997  cotr  5167  issref  5168  asymref  5171  intirr  5172  sb8iota  5343  dffun2  5385  dffun4  5386  dffun6f  5388  dffun4f  5391  dffun7  5402  funopab  5410  funcnv2  5439  funcnv  5440  funcnveq  5442  fun2cnv  5443  fun11  5446  fununi  5447  funcnvuni  5448  funimaexglem  5462  fnres  5498  fnopabg  5505  rexrnmpt  5845  dff13  5968  iotaexel  6037  oprabidlem  6110  eqoprab2b  6140  mpo2eqb  6192  ralrnmpo  6197  dfer2  6802  pw1dc0el  7212  fiintim  7232  omniwomnimkv  7501  ltexprlemdisj  7967  recexprlemdisj  7991  nnwosdc  12799  isprm2  12878  ivthdich  15737  bj-stal  16760  bj-nfalt  16775  bdceq  16851  bdcriota  16892  bj-axempty2  16903  bj-vprc  16905  bdinex1  16908  bj-zfpair2  16919  bj-uniex2  16925  bj-ssom  16945  bj-inf2vnlem2  16980  ss1oel2o  17000  dfrals2  17104  alsbii  17115  dfralseu2  17138  alseubii  17147