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  3793  snssb  3800  snsssn  3838  dfnfc2  3905  uni0b  3912  unissb  3917  elintrab  3934  ssintrab  3945  intun  3953  intpr  3954  dfiin2g  3997  iunss  4005  dfdisj2  4060  cbvdisj  4068  disjnim  4072  dftr2  4183  dftr5  4184  trint  4196  zfnuleu  4207  vnex  4214  inex1  4217  repizf2lem  4244  axpweq  4254  zfpow  4258  axpow2  4259  axpow3  4260  exmid01  4281  zfpair2  4293  ssextss  4305  frirrg  4438  sucel  4498  zfun  4522  uniex2  4524  setindel  4627  setind  4628  elirr  4630  en2lp  4643  zfregfr  4663  tfi  4671  peano5  4687  ssrel  4804  ssrel2  4806  eqrelrel  4817  reliun  4837  raliunxp  4860  relop  4869  dmopab3  4933  dm0rn0  4937  reldm0  4938  cotr  5106  issref  5107  asymref  5110  intirr  5111  sb8iota  5282  dffun2  5324  dffun4  5325  dffun6f  5327  dffun4f  5330  dffun7  5341  funopab  5349  funcnv2  5377  funcnv  5378  funcnveq  5380  fun2cnv  5381  fun11  5384  fununi  5385  funcnvuni  5386  funimaexglem  5400  fnres  5436  fnopabg  5443  rexrnmpt  5771  dff13  5885  iotaexel  5952  oprabidlem  6025  eqoprab2b  6053  mpo2eqb  6105  ralrnmpo  6110  dfer2  6671  pw1dc0el  7061  fiintim  7081  omniwomnimkv  7322  ltexprlemdisj  7781  recexprlemdisj  7805  nnwosdc  12546  isprm2  12625  ivthdich  15312  bj-stal  16043  bj-nfalt  16058  bdceq  16135  bdcriota  16176  bj-axempty2  16187  bj-vprc  16189  bdinex1  16192  bj-zfpair2  16203  bj-uniex2  16209  bj-ssom  16229  bj-inf2vnlem2  16264  ss1oel2o  16285