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 206  ∀wal 1539

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 207

This theorem is referenced by:  2albii  1821  3albii  1822  hbxfrbi  1826  alex  1827  2nalexn  1829  2exnaln  1830  imnang  1843  alexn  1846  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  2005  2sb6  2091  sbrimvw  2096  sbbiiev  2097  alrot3  2165  alrot4  2166  sbal  2174  sbalv  2175  19.21-2  2216  19.32  2240  19.31  2241  equsalv  2274  sbn  2286  sbrim  2310  sbnfOLD  2318  aaan  2337  pm11.53  2350  19.12vv  2351  sb8v  2357  sb8f  2358  cbvsbvf  2367  equsal  2421  2sb6rf  2477  sbcom3  2510  sb8eulem  2598  eu1  2610  2mo2  2647  2eu1  2651  2eu1v  2652  2eu3  2654  euae  2660  nulmo  2713  eqabbw  2809  eqabcbw  2810  hblem  2867  hblemg  2868  eqabcb  2876  nfceqi  2895  eqabf  2928  ralbii2  3078  r2allem  3124  r3al  3174  r19.21t  3230  r19.23t  3232  ralcom4  3262  cbvralsvw  3287  sbralie  3322  sbralieOLD  3324  rabbi  3429  rabid2f  3430  rabid2im  3431  eqv  3450  eqvf  3451  abv  3452  abvALT  3453  ralv  3467  ceqsralt  3475  ceqsal  3478  ceqsalv  3480  rspc2gv  3586  ralxpxfr2d  3600  clel2g  3613  clel4g  3617  elabgtOLDOLD  3628  ralab  3651  ralrab2  3656  euind  3682  reu2  3683  reu3  3685  rmo4  3688  reu8  3691  rmo3f  3692  rmoim  3698  2reuswap  3704  2reuswap2  3705  reuind  3711  2reu5lem2  3714  2reu5lem3  3715  2rmoswap  3719  sbccomlem  3819  rmo2  3837  rmo3  3839  rmoanim  3844  dfss2  3919  ss2ab  4013  ss2rab  4021  rabss  4022  ss2rabd  4024  uniiunlem  4039  dfdif3OLD  4070  ssequn1  4138  unss  4142  ralunb  4149  ssin  4191  eq0f  4299  eq0  4302  eq0ALT  4303  ssdif0  4318  inssdif0  4326  ab0w  4331  ab0  4332  ab0ALT  4333  ab0orv  4335  disj  4402  disj3  4406  ssundif  4440  ralf0  4450  ralidmw  4469  ralidm  4470  pwss  4577  rabsssn  4625  rabeqsnd  4626  ralsnsg  4627  ralsng  4632  disjsn  4668  snssb  4739  pwpw0  4769  dfnfc2  4885  unissb  4896  elintrab  4915  ssintrab  4926  intun  4935  intprg  4936  dfiin2g  4986  iunssf  4998  iunssfOLD  4999  iunss  5000  iunssOLD  5001  dfdisj2  5067  cbvdisj  5075  cbvdisjv  5076  disjor  5080  dftr2  5207  dftr5  5209  axrep1  5225  axrep4v  5229  axrep4  5230  axrep5  5232  axrep6  5233  axrep6OLD  5234  axsepgfromrep  5239  axnulALT  5249  vnex  5259  inex1  5262  axpweq  5296  zfpow  5311  axpow2  5312  nfnid  5320  dtruALT  5333  reusv2lem4  5346  zfpair2  5378  el  5387  ssextss  5401  moabexOLD  5407  dffr6  5580  dffr2  5585  dffr2ALT  5586  dfepfr  5608  frinxp  5707  ssrel2  5734  eqrelrel  5746  raliunxp  5788  relop  5799  dmopab3  5868  dm0rn0  5873  dm0rn0OLD  5874  reldm0  5877  rnopab3  5905  iresn0n0  6013  dffr3  6058  cotrg  6068  idrefALT  6070  asymref  6073  asymref2  6074  intirr  6075  dffr4  6278  sucel  6393  sb8iota  6459  dffun6  6503  dffun3  6504  dffun4  6505  dffun5  6506  dffun6f  6507  dffun7  6519  funopab  6527  funcnv2  6560  funcnv  6561  fun2cnv  6563  fun11  6566  fununi  6567  fnres  6619  mptfnf  6627  fnopabg  6629  tz6.12-2  6821  brprcneu  6824  brprcneuALT  6825  dffv2  6929  fvn0ssdmfun  7019  dff13  7200  fnssintima  7308  eqoprab2bw  7428  eqoprab2b  7429  mpo2eqb  7490  ralrnmpo  7497  imaeqalov  7597  zfun  7681  uniex2  7683  funcnvuni  7874  ralxp3f  8079  frpoins3xpg  8082  frpoins3xp3g  8083  xpord3inddlem  8096  dfer2  8636  fiint  9227  marypha1lem  9336  marypha2lem3  9340  inf2  9532  axinf2  9549  ttrclss  9629  scottexs  9799  scott0s  9800  aceq1  10027  dfac4  10032  dfac7  10043  dfac0  10044  dfac1  10045  dfac10  10048  dfac10c  10049  dfac10b  10050  kmlem4  10064  kmlem12  10072  kmlem14  10074  kmlem15  10075  kmlem16  10076  dfackm  10077  ac6n  10395  axpowndlem3  10510  zfcndrep  10525  zfcndun  10526  zfcndpow  10527  axgroth5  10735  axgroth2  10736  axgroth4  10743  grothprim  10745  sstskm  10753  fimaxre3  12088  infm3  12101  nnwos  12828  cotr2g  14899  brtrclfv  14925  trclfvcotr  14932  rpnnen2lem12  16150  isprm2  16609  vdwmc2  16907  pgpfac1  20011  pgpfac  20015  iunocv  21636  2ndcdisj2  23401  hausdiag  23589  rnelfmlem  23896  alexsubALTlem3  23993  cnextfun  24008  itg2leub  25691  eqcuts2  27782  addsuniflem  27997  mulsuniflem  28145  onsfi  28352  mpteleeOLD  28968  nmoubi  30847  nmobndseqi  30854  nmobndseqiALT  30855  isch2  31298  isch3  31316  choc0  31401  nmopub  31983  nmfnleub  32000  xfree2  32520  mo5f  32563  nmo  32564  reuxfrdf  32565  rabsspr  32576  rabsstp  32577  inpr0  32607  cbvdisjf  32646  disjorf  32654  ssrelf  32693  funcnvmpt  32745  funcnv5mpt  32746  ssdifidlprm  33539  ballotlem2  34646  bnj89  34877  bnj115  34881  bnj1143  34946  bnj110  35014  bnj611  35074  bnj864  35078  bnj865  35079  bnj1000  35097  bnj978  35105  bnj1049  35130  bnj1052  35131  bnj1090  35135  bnj1030  35143  bnj1133  35145  bnj1171  35156  bnj1172  35157  bnj1174  35159  bnj1176  35161  bnj1204  35168  bnj1253  35173  bnj1388  35189  bnj1523  35227  fineqvrep  35270  fineqvpow  35271  axreg  35283  axregscl  35284  axregs  35295  vonf1owev  35302  axrepprim  35896  axunprim  35897  axpowprim  35898  axinfprim  35900  axacprim  35901  untuni  35903  dffr5  35948  elintfv  35959  dfon2lem8  35982  dfon2lem9  35983  19.12b  35993  brtxpsd3  36088  dfom5b  36104  dffun10  36106  disjeq1i  36386  ss-ax8  36419  cbvdisjvw2  36429  mh-setind  36666  regsfromregtr  36668  regsfromsetind  36669  regsfromunir1  36670  bj-notalbii  36814  bj-df-sb  36853  bj-ssbeq  36854  bj-ax12ssb  36859  bj-hbext  36911  bj-nfalt  36912  bj-substax12  36922  bj-nnfalt  36967  bj-nnfext  36968  ax11-pm2  37037  bj-sblem  37045  eliminable-veqab  37067  eliminable-abeqv  37068  eliminable-abeqab  37069  bj-ralvw  37080  bj-sbeq  37102  bj-nfcf  37124  bj-snsetex  37164  bj-rcleqf  37226  bj-clex  37232  fvineqsneq  37613  wl-equsalvw  37739  wl-equsalcom  37744  wl-sb9v  37750  wl-sb8eft  37752  wl-sb8et  37754  wl-2sb6d  37759  wl-alanbii  37770  wl-sb8eut  37779  wl-sb8eutv  37780  poimirlem25  37842  poimirlem30  37847  heibor1lem  38006  sbcalfi  38313  mpobi123f  38359  mptbi12f  38363  ineccnvmo  38546  alrmomorn  38547  cocossss  38695  cossssid3  38728  cossssid4  38729  cosscnvssid4  38736  trcoss2  38743  dfeldisj4  38975  dfeldisj5  38976  disjres  38999  dvelimf-o  39185  axc11n-16  39194  pmapglbx  40025  sn-axrep5v  42469  abbibw  42916  dford4  43267  unielss  43456  onsupmaxb  43477  rp-fakeinunass  43752  rababg  43811  elmapintrab  43813  elinintrab  43814  undmrnresiss  43841  clss2lem  43848  cotrintab  43851  elintima  43890  relexp0eq  43938  dfhe3  44012  snhesn  44023  psshepw  44025  dffrege76  44176  frege77  44177  frege110  44210  dffrege115  44215  frege116  44216  frege118  44218  frege131  44231  ntrneikb  44331  ismnuprim  44531  rr-grothprimbi  44532  ismnushort  44538  rr-grothshortbi  44540  pm10.541  44604  pm10.542  44605  19.21vv  44613  19.31vv  44621  19.28vv  44623  pm11.62  44631  axc11next  44643  pm13.196a  44651  2sbc6g  44652  elnev  44674  hbexgVD  45142  dfac5prim  45227  permaxext  45242  permaxrep  45243  permaxpow  45246  permac8prim  45251  rabssf  45359  sinnpoly  47133  2rexsb  47343  dfich2  47700  ichal  47708  spr0nelg  47718  mo0sn  49057  dffun3f  49923  setrec1lem2  49929  setrec2  49936  setis  49939  alimp-surprise  50021  alimp-no-surprise  50022