Theorem albii 1820

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

Syntax hints:   ↔ wb 208  ∀wal 1535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810

This theorem depends on definitions:  df-bi 209

This theorem is referenced by:  2albii  1821  hbxfrbi  1825  alex  1826  2nalexn  1828  2exnaln  1829  imnang  1842  alexn  1845  nfnbi  1855  19.26-2  1872  19.26-3an  1873  19.43OLD  1884  albiim  1890  2albiim  1891  empty  1907  19.32v  1941  19.31v  1942  19.23vv  1944  pm11.53v  1945  19.12vvv  1995  equsalvw  2010  2sb6  2094  sbrimvlem  2101  sbcom3vv  2106  alrot3  2164  alrot4  2165  sbal  2166  sbalv  2167  19.21-2  2209  19.32  2235  19.31  2236  equsalv  2268  sbn  2287  aaan  2353  pm11.53  2367  19.12vv  2368  equsal  2439  2sb6rf  2497  sbcom3  2548  sb8eulem  2684  eu1  2694  2mo2  2732  2eu1  2735  2eu1v  2736  2eu3  2738  euae  2745  nulmo  2798  hblem  2943  hblemg  2944  abeq2  2945  abeq1  2946  abbiOLD  2955  nfcrii  2970  nfceqi  2973  abeq2f  3013  abeq2fOLD  3014  ralbii2  3163  ralanidOLD  3169  r19.21v  3175  r2allem  3200  r3al  3202  r19.21t  3214  ralcom4  3235  r19.23t  3313  rabid2  3381  rabid2f  3382  rabbi  3383  eqv  3502  eqvf  3503  abv  3504  ralv  3519  ceqsralt  3528  rspc2gv  3632  ralxpxfr2d  3639  ralab  3684  ralrab2  3690  euind  3715  reu2  3716  reu3  3718  rmo4  3721  reu8  3724  rmo3f  3725  rmoim  3731  2reuswap  3737  2reuswap2  3738  reuind  3744  2reu5lem2  3747  2reu5lem3  3748  2rmoswap  3752  rmo2  3870  rmo3  3872  rmo3OLD  3873  rmoanim  3878  dfss2  3955  ss2ab  4039  ss2rab  4047  rabss  4048  uniiunlem  4061  dfdif3  4091  ssequn1  4156  unss  4160  ralunb  4167  ssin  4207  eq0f  4305  ssdif0  4323  inssdif0  4329  ab0  4333  disj  4399  disj3  4403  ssundif  4433  ralf0  4457  pwss  4564  rabsssn  4607  ralsnsg  4608  disjsn  4647  snssg  4717  pwpw0  4746  pwsnOLD  4831  dfnfc2  4860  unissb  4870  elintrab  4888  ssintrab  4899  intun  4908  intpr  4909  dfiin2g  4957  iunss  4969  dfdisj2  5033  cbvdisj  5041  disjor  5046  dftr2  5174  dftr5  5175  axrep1  5191  axrep5  5196  axrep6  5197  axsepgfromrep  5201  axnulALT  5208  vnex  5218  inex1  5221  axpweq  5265  zfpow  5267  axpow2  5268  axpow3  5269  nfnid  5276  dtruALT  5289  reusv2lem4  5302  zfpair2  5331  dtruALT2  5336  ssextss  5346  moabex  5351  dffr2  5520  dfepfr  5540  frinxp  5634  ssrel2  5659  eqrelrel  5670  reliun  5689  raliunxp  5710  relop  5721  dmopab3  5788  dm0rn0  5795  reldm0  5798  iresn0n0  5923  dffr3  5962  cotrg  5971  idrefALT  5973  asymref  5976  asymref2  5977  intirr  5978  dffr4  6164  sucel  6264  sb8iota  6325  dffun2  6365  dffun3  6366  dffun4  6367  dffun5  6368  dffun6f  6369  dffun7  6382  funopab  6390  funcnv2  6422  funcnv  6423  fun2cnv  6425  fun11  6428  fununi  6429  fnres  6474  mptfnf  6483  fnopabg  6485  brprcneu  6662  dffv2  6756  fvn0ssdmfun  6842  dff13  7013  eqoprab2bw  7224  eqoprab2b  7225  mpo2eqb  7283  ralrnmpo  7289  zfun  7462  uniex2  7464  funcnvuni  7636  dfer2  8290  fiint  8795  marypha1lem  8897  marypha2lem3  8901  inf2  9086  axinf2  9103  scottexs  9316  scott0s  9317  aceq1  9543  dfac4  9548  dfac7  9558  dfac0  9559  dfac1  9560  dfac10  9563  dfac10c  9564  dfac10b  9565  kmlem4  9579  kmlem12  9587  kmlem14  9589  kmlem15  9590  kmlem16  9591  dfackm  9592  ac6n  9907  axpowndlem3  10021  zfcndrep  10036  zfcndun  10037  zfcndpow  10038  axgroth5  10246  axgroth2  10247  axgroth4  10254  grothprim  10256  sstskm  10264  fimaxre3  11587  infm3  11600  nnwos  12316  cotr2g  14336  brtrclfv  14362  trclfvcotr  14369  rpnnen2lem12  15578  isprm2  16026  vdwmc2  16315  pgpfac1  19202  pgpfac  19206  iunocv  20825  2ndcdisj2  22065  hausdiag  22253  rnelfmlem  22560  alexsubALTlem3  22657  cnextfun  22672  itg2leub  24335  mptelee  26681  nmoubi  28549  nmobndseqi  28556  nmobndseqiALT  28557  isch2  29000  isch3  29018  choc0  29103  nmopub  29685  nmfnleub  29702  xfree2  30222  nelbOLD  30232  moel  30252  mo5f  30253  nmo  30254  reuxfrdf  30255  rabeqsnd  30264  inpr0  30292  cbvdisjf  30321  disjorf  30329  ssrelf  30366  funcnvmpt  30412  funcnv5mpt  30413  ballotlem2  31746  bnj89  31991  bnj115  31995  bnj1143  32062  bnj110  32130  bnj611  32190  bnj864  32194  bnj865  32195  bnj1000  32213  bnj978  32221  bnj1049  32246  bnj1052  32247  bnj1090  32251  bnj1030  32259  bnj1133  32261  bnj1171  32272  bnj1172  32273  bnj1174  32275  bnj1176  32277  bnj1204  32284  bnj1253  32289  bnj1388  32305  bnj1523  32343  axrepprim  32928  axunprim  32929  axpowprim  32930  axinfprim  32932  axacprim  32933  untuni  32935  dffr5  32989  elintfv  33007  dfon2lem8  33035  dfon2lem9  33036  19.12b  33046  brtxpsd3  33357  dfom5b  33373  dffun10  33375  bj-notalbii  33948  bj-ssbeq  33986  bj-ax12ssb  33991  bj-hbext  34044  bj-nfalt  34045  bj-nnfalt  34095  bj-nnfext  34096  ax11-pm2  34159  bj-sbnf  34164  bj-sblem  34168  bj-ralvw  34198  bj-sbeq  34221  bj-nfcf  34245  bj-snsetex  34278  bj-rcleqf  34340  fvineqsneq  34696  wl-equsalvw  34793  wl-equsalcom  34797  wl-sb8et  34804  wl-2sb6d  34809  wl-alanbii  34820  wl-sb8eut  34828  wl-dfralsb  34852  wl-dfralflem  34853  wl-dfralv  34856  wl-dfrexex  34865  wl-dfrexsb  34866  wl-dfrmosb  34868  wl-dfrmov  34869  poimirlem25  34932  poimirlem30  34937  heibor1lem  35102  sbcalfi  35409  mpobi123f  35455  mptbi12f  35459  3albii  35524  ineccnvmo  35626  alrmomorn  35627  cocossss  35696  cossssid3  35724  cossssid4  35725  cosscnvssid4  35732  trcoss2  35739  dfeldisj4  35968  dfeldisj5  35969  dvelimf-o  36080  axc11n-16  36089  pmapglbx  36920  sn-axrep5v  39157  dford4  39675  rp-fakeinunass  39930  rababg  39982  elmapintrab  39985  elinintrab  39986  undmrnresiss  40013  clss2lem  40020  cotrintab  40023  elintima  40047  ss2iundf  40053  relexp0eq  40095  dfhe3  40170  snhesn  40181  psshepw  40183  dffrege76  40334  frege77  40335  frege110  40368  dffrege115  40373  frege116  40374  frege118  40376  frege131  40389  ntrneikb  40493  ismnuprim  40679  rr-grothprimbi  40680  pm10.541  40748  pm10.542  40749  19.21vv  40757  19.31vv  40765  19.28vv  40767  pm11.62  40775  axc11next  40787  pm13.196a  40795  2sbc6g  40796  elnev  40819  hbexgVD  41289  iunssf  41401  rabssf  41434  2rexsb  43348  dfich2  43662  dfich2ai  43663  ichal  43676  spr0nelg  43687  dffun3f  44834  setrec1lem2  44840  setrec2  44847  setis  44849  alimp-surprise  44930  alimp-no-surprise  44931