Theorem albii 1821

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

Syntax hints:   ↔ wb 206  ∀wal 1540

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

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  2albii  1822  3albii  1823  hbxfrbi  1827  alex  1828  2nalexn  1830  2exnaln  1831  imnang  1844  alexn  1847  19.26-2  1873  19.26-3an  1874  19.43OLD  1885  albiim  1891  2albiim  1892  empty  1908  19.32v  1942  19.31v  1943  19.23vv  1945  pm11.53v  1946  19.12vvv  1996  equsalvw  2006  2sb6  2092  sbrimvw  2097  sbbiiev  2098  alrot3  2166  alrot4  2167  sbal  2175  sbalv  2176  19.21-2  2217  19.32  2241  19.31  2242  equsalv  2275  sbn  2287  sbrim  2311  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  3079  r2allem  3125  r3al  3175  r19.21t  3231  r19.23t  3233  ralcom4  3263  cbvralsvw  3288  sbralie  3315  sbralieOLD  3317  rabbi  3419  rabid2f  3420  rabid2im  3421  eqv  3439  eqvf  3440  abv  3441  abvALT  3442  ralv  3456  ceqsralt  3464  ceqsal  3467  ceqsalv  3469  rspc2gv  3574  ralxpxfr2d  3588  clel2g  3601  clel4g  3605  elabgtOLDOLD  3616  ralab  3639  ralrab2  3644  euind  3670  reu2  3671  reu3  3673  rmo4  3676  reu8  3679  rmo3f  3680  rmoim  3686  2reuswap  3692  2reuswap2  3693  reuind  3699  2reu5lem2  3702  2reu5lem3  3703  2rmoswap  3707  sbccomlem  3807  rmo2  3825  rmo3  3827  rmoanim  3832  dfss2  3907  ss2ab  4001  ss2rab  4009  rabss  4010  ss2rabd  4012  uniiunlem  4027  dfdif3OLD  4058  ssequn1  4126  unss  4130  ralunb  4137  ssin  4179  eq0f  4287  eq0  4290  eq0ALT  4291  ssdif0  4306  inssdif0  4314  ab0w  4319  ab0  4320  ab0ALT  4321  ab0orv  4323  disj  4390  disj3  4394  ssundif  4427  ralf0  4437  ralidmw  4456  ralidm  4457  pwss  4564  rabsssn  4612  rabeqsnd  4613  ralsnsg  4614  ralsng  4619  disjsn  4655  snssb  4726  pwpw0  4756  dfnfc2  4872  unissb  4883  elintrab  4902  ssintrab  4913  intun  4922  intprg  4923  dfiin2g  4973  iunssf  4985  iunssfOLD  4986  iunss  4987  iunssOLD  4988  dfdisj2  5054  cbvdisj  5062  cbvdisjv  5063  disjor  5067  dftr2  5194  dftr5  5196  axrep1  5213  axrep4v  5217  axrep4  5218  axrep5  5220  axrep6  5221  axrep6OLD  5222  zfrep6  5224  axsepgfromrep  5229  axnulALT  5239  vnexOLD  5253  inex1  5258  axpweq  5292  zfpow  5308  axpow2  5309  nfnid  5317  dtruALT  5330  reusv2lem4  5343  zfpair2  5376  prex  5380  elOLD  5391  ssextss  5405  moabexOLD  5411  dffr6  5587  dffr2  5592  dffr2ALT  5593  dfepfr  5615  frinxp  5714  ssrel2  5741  eqrelrel  5753  raliunxp  5794  relop  5805  dmopab3  5874  dm0rn0  5879  dm0rn0OLD  5880  reldm0  5883  rnopab3  5911  iresn0n0  6019  dffr3  6064  cotrg  6074  idrefALT  6076  asymref  6079  asymref2  6080  intirr  6081  dffr4  6284  sucel  6399  sb8iota  6465  dffun6  6509  dffun3  6510  dffun4  6511  dffun5  6512  dffun6f  6513  dffun7  6525  funopab  6533  funcnv2  6566  funcnv  6567  fun2cnv  6569  fun11  6572  fununi  6573  fnres  6625  mptfnf  6633  fnopabg  6635  tz6.12-2  6827  brprcneu  6830  brprcneuALT  6831  dffv2  6935  funcnvmpt  6949  fvn0ssdmfun  7026  dff13  7209  fnssintima  7317  eqoprab2bw  7437  eqoprab2b  7438  mpo2eqb  7499  ralrnmpo  7506  imaeqalov  7606  zfun  7690  uniex2  7692  funcnvuni  7883  ralxp3f  8087  frpoins3xpg  8090  frpoins3xp3g  8091  xpord3inddlem  8104  dfer2  8644  fiint  9237  marypha1lem  9346  marypha2lem3  9350  inf2  9544  axinf2  9561  ttrclss  9641  scottexs  9811  scott0s  9812  aceq1  10039  dfac4  10044  dfac7  10055  dfac0  10056  dfac1  10057  dfac10  10060  dfac10c  10061  dfac10b  10062  kmlem4  10076  kmlem12  10084  kmlem14  10086  kmlem15  10087  kmlem16  10088  dfackm  10089  ac6n  10407  axpowndlem3  10522  zfcndrep  10537  zfcndun  10538  zfcndpow  10539  axgroth5  10747  axgroth2  10748  axgroth4  10755  grothprim  10757  sstskm  10765  fimaxre3  12102  infm3  12115  nnwos  12865  cotr2g  14938  brtrclfv  14964  trclfvcotr  14971  rpnnen2lem12  16192  isprm2  16651  vdwmc2  16950  pgpfac1  20057  pgpfac  20061  iunocv  21661  2ndcdisj2  23422  hausdiag  23610  rnelfmlem  23917  alexsubALTlem3  24014  cnextfun  24029  itg2leub  25701  eqcuts2  27778  addsuniflem  27993  mulsuniflem  28141  onsfi  28348  mpteleeOLD  28964  nmoubi  30843  nmobndseqi  30850  nmobndseqiALT  30851  isch2  31294  isch3  31312  choc0  31397  nmopub  31979  nmfnleub  31996  xfree2  32516  mo5f  32558  nmo  32559  reuxfrdf  32560  rabsspr  32571  rabsstp  32572  inpr0  32602  cbvdisjf  32641  disjorf  32649  ssrelf  32688  funcnv5mpt  32740  ssdifidlprm  33518  ballotlem2  34633  bnj89  34864  bnj115  34868  bnj1143  34932  bnj110  35000  bnj611  35060  bnj864  35064  bnj865  35065  bnj1000  35083  bnj978  35091  bnj1049  35116  bnj1052  35117  bnj1090  35121  bnj1030  35129  bnj1133  35131  bnj1171  35142  bnj1172  35143  bnj1174  35145  bnj1176  35147  bnj1204  35154  bnj1253  35159  bnj1388  35175  bnj1523  35213  axnulALT2  35224  fineqvrep  35258  fineqvpow  35259  axreg  35271  axregscl  35272  axregs  35283  vonf1owev  35290  axrepprim  35884  axunprim  35885  axpowprim  35886  axinfprim  35888  axacprim  35889  untuni  35891  dffr5  35936  elintfv  35947  dfon2lem8  35970  dfon2lem9  35971  19.12b  35981  brtxpsd3  36076  dfom5b  36092  dffun10  36094  disjeq1i  36374  ss-ax8  36407  cbvdisjvw2  36417  mh-setind  36718  regsfromregtco  36720  regsfromsetind  36721  regsfromunir1  36722  mh-prprimbi  36725  mh-unprimbi  36726  mh-infprim1bi  36728  mh-infprim2bi  36729  mh-infprim3bi  36730  bj-notalbii  36894  bj-cbvaew  36938  bj-ssbeq  36947  bj-ax12ssb  36952  bj-nfalt  37010  bj-substax12  37021  bj-nnfalt  37087  bj-nnfext  37088  ax11-pm2  37143  bj-sblem  37151  eliminable-veqab  37173  eliminable-abeqv  37174  eliminable-abeqab  37175  bj-ralvw  37186  bj-sbeq  37208  bj-nfcf  37230  bj-snsetex  37270  bj-rcleqf  37332  bj-clex  37338  bj-rep  37380  bj-axseprep  37381  fvineqsneq  37728  wl-equsalvw  37863  wl-equsalcom  37868  wl-sb9v  37874  wl-sb8eft  37876  wl-sb8et  37878  wl-2sb6d  37883  wl-alanbii  37894  wl-sb8eut  37903  wl-sb8eutv  37904  poimirlem25  37966  poimirlem30  37971  heibor1lem  38130  sbcalfi  38437  mpobi123f  38483  mptbi12f  38487  ineccnvmo  38678  alrmomorn  38679  ralmo  38681  ralrmo3  38685  cocossss  38847  cossssid3  38880  cossssid4  38881  cosscnvssid4  38888  trcoss2  38895  dfeldisj4  39133  dfeldisj5  39134  disjres  39165  dvelimf-o  39375  axc11n-16  39384  pmapglbx  40215  sn-axrep5v  42658  abbibw  43110  dford4  43457  unielss  43646  onsupmaxb  43667  rp-fakeinunass  43942  rababg  44001  elmapintrab  44003  elinintrab  44004  undmrnresiss  44031  clss2lem  44038  cotrintab  44041  elintima  44080  relexp0eq  44128  dfhe3  44202  snhesn  44213  psshepw  44215  dffrege76  44366  frege77  44367  frege110  44400  dffrege115  44405  frege116  44406  frege118  44408  frege131  44421  ntrneikb  44521  ismnuprim  44721  rr-grothprimbi  44722  ismnushort  44728  rr-grothshortbi  44730  pm10.541  44794  pm10.542  44795  19.21vv  44803  19.31vv  44811  19.28vv  44813  pm11.62  44821  axc11next  44833  pm13.196a  44841  2sbc6g  44842  elnev  44864  hbexgVD  45332  dfac5prim  45417  permaxext  45432  permaxrep  45433  permaxpow  45436  permac8prim  45441  rabssf  45549  sinnpoly  47339  2rexsb  47549  dfich2  47918  ichal  47926  spr0nelg  47936  mo0sn  49291  dffun3f  50157  setrec1lem2  50163  setrec2  50170  setis  50173  alimp-surprise  50255  alimp-no-surprise  50256