Theorem albii 1851

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

This proof depends on syntax axioms:   ↔ wb 209  ∀wal 1567

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841

This proof depends on definitions:  df-bi 210

This theorem is used by:  2albii  1852  3albii  1853  hbxfrbi  1857  alex  1858  2nalexn  1860  2exnaln  1861  imnang  1874  alexn  1877  19.26-2  1903  19.26-3an  1904  19.43OLD  1915  albiim  1921  2albiim  1922  empty  1938  19.32v  1972  19.31v  1973  19.23vv  1975  pm11.53v  1976  19.12vvv  2026  equsalvw  2036  2sb6  2122  sbrimvwOLD  2128  sbbiiev  2129  alrot3  2196  alrot4  2197  sbal  2205  sbalv  2206  19.21-2  2245  19.32  2269  19.31  2270  equsalv  2301  sbn  2313  sbrim  2337  aaan  2362  pm11.53  2375  19.12vv  2376  sb8v  2382  sb8f  2383  cbvsbvf  2392  equsal  2446  2sb6rf  2502  sbcom3  2535  sb8eulem  2623  eu1  2635  2mo2  2672  2eu1  2675  2eu1v  2676  2eu3  2678  euae  2684  nulmo  2737  eqabbw  2833  eqabcbw  2834  hblem  2891  hblemg  2892  eqabcb  2900  nfceqi  2919  eqabf  2951  ralbii2  3104  r2allem  3150  r3al  3200  r19.21t  3256  r19.23t  3258  ralcom4  3288  cbvralsvw  3313  sbralie  3338  sbralieOLD  3340  rabbi  3441  rabid2f  3442  rabid2im  3443  eqv  3460  eqvf  3461  abv  3462  abvALT  3463  ralv  3476  ceqsralt  3484  ceqsal  3487  ceqsalv  3489  rspc2gv  3585  ralxpxfr2d  3599  clel2g  3612  clel4g  3616  ralab  3650  ralrab2  3655  euind  3681  reu2  3682  reu3  3684  rmo4  3687  reu8  3690  rmo3f  3691  rmoim  3697  2reuswap  3703  2reuswap2  3704  reuind  3710  2reu5lem2  3713  2reu5lem3  3714  2rmoswap  3718  sbccomlem  3816  rmo2  3833  rmo3  3835  rmoanim  3841  ss2ab  3986  ss2rab  3994  rabss  3995  ss2rabd  3997  uniiunlem  4012  dfss2  4094  ssin  4135  ssequn1  4184  unss  4188  ralunb  4195  eq0f  4293  eq0  4296  eq0ALT  4297  ssdif0  4313  inssdif0OLD  4322  ab0w  4327  ab0  4328  ab0ALT  4329  ab0orv  4331  disj  4402  disj3  4406  ssundif  4442  ralf0  4452  ralidmw  4471  ralidm  4472  pwss  4581  rabsssn  4625  rabeqsnd  4626  ralsnsg  4627  ralsng  4632  disjsn  4668  snssb  4739  pwpw0  4830  dfnfc2  4888  unissb  4900  elintrab  4919  ssintrab  4930  intun  4939  intprg  4940  dfiin2g  4988  iunssf  5000  iunssfOLD  5001  iunss  5002  iunssOLD  5003  dfdisj2  5071  cbvdisj  5079  cbvdisjv  5080  disjor  5084  dftr2  5213  dftr5  5215  axrep1  5232  axrep4v  5236  axrep4  5237  axrep5  5238  axrep6  5239  zfrep6  5241  axsepgfromrep  5246  axnulALT  5257  vnexOLD  5271  inex1  5276  axpweq  5311  zfpow  5327  axpow2  5328  nfnid  5336  dtruALT  5349  reusv2lem4  5362  zfpair2  5391  prex  5395  el.OLD  5406  ssextss  5420  moabexOLD  5426  dffr6  5606  dffr2  5611  dffr2ALT  5612  dfepfr  5634  frinxp  5733  ssrel2  5760  eqrelrel  5772  raliunxp  5815  relop  5827  dmopab3  5900  dm0rn0  5905  dm0rn0OLD  5906  reldm0  5909  rnopab3  5937  iresn0n0  6045  dffr3  6096  cotrg  6104  idrefALT  6106  asymref  6109  asymref2  6110  intirr  6111  dffr4  6323  sucel  6439  sb8iota  6505  dffun6  6550  dffun3  6551  dffun4  6552  dffun5  6553  dffun6f  6554  dffun7  6568  funopab  6576  funcnv2  6609  funcnv  6610  fun2cnv  6612  fun11  6615  fununi  6616  fnres  6667  mptfnf  6675  fnopabg  6677  tz6.12-2  6873  brprcneu  6876  brprcneuALT  6877  dffv2  6981  funcnvmpt  6996  fvn0ssdmfun  7075  dff13  7259  fnssintima  7373  eqoprab2bw  7491  eqoprab2b  7492  mpo2eqb  7553  ralrnmpo  7560  imaeqalov  7661  zfun  7753  uniex2  7755  uniex2OLD  7756  funcnvuni  7945  ralxp3f  8157  frpoins3xpg  8160  frpoins3xp3g  8161  xpord3inddlem  8174  dfer2  8722  fiint  9322  marypha1lem  9429  marypha2lem3  9433  inf2  9628  axinf2  9645  ttrclss  9725  scottexsOLD  9947  scott0bsOLD  9949  setrec1lem2  9971  dffun3f  9979  setrec2  9981  aceq1  10200  dfac4  10205  dfac7  10215  dfac0  10216  dfac1  10217  dfac10  10220  dfac10c  10221  dfac10b  10222  kmlem4  10236  kmlem12  10244  kmlem14  10246  kmlem15  10247  kmlem16  10248  dfackm  10249  ac6n  10567  axpowndlem3  10688  zfcndrep  10703  zfcndun  10704  zfcndpow  10705  axgroth5  10913  axgroth2  10914  axgroth4  10921  grothprim  10923  sstskm  10931  fimaxre3  12267  infm3  12280  nnwos  13046  cotr2g  15135  brtrclfv  15161  trclfvcotr  15168  rpnnen2lem12  16399  isprm2  16863  vdwmc2  17163  pgpfac1  20302  pgpfac  20306  ssdifidlprm  21648  iunocv  21993  2ndcdisj2  23782  hausdiag  23970  rnelfmlem  24277  alexsubALTlem3  24374  cnextfun  24389  itg2leub  26061  eqcuts2  28178  addsuniflem  28393  mulsuniflem  28541  onsfi  28748  mpteleeOLD  29479  nmoubi  31380  nmobndseqi  31387  nmobndseqiALT  31388  isch2  31831  isch3  31849  choc0  31934  nmopub  32516  nmfnleub  32533  xfree2  33095  mo5f  33133  nmo  33134  reuxfrdf  33135  rabsspr  33145  rabsstp  33146  inpr0  33176  cbvdisjf  33213  disjorf  33221  ssrelf  33257  funcnv5mpt  33309  ballotlem2  35168  bnj89  35399  bnj115  35403  bnj1143  35467  bnj110  35535  bnj611  35595  bnj864  35599  bnj865  35600  bnj1000  35618  bnj978  35626  bnj1049  35651  bnj1052  35652  bnj1090  35656  bnj1030  35664  bnj1133  35666  bnj1171  35677  bnj1172  35678  bnj1174  35680  bnj1176  35682  bnj1204  35689  bnj1253  35694  bnj1388  35710  bnj1523  35748  axnulALT2  35761  fineqvrep  35839  fineqvpow  35840  axreg  35852  axregscl  35853  axregs  35864  axpowg  35871  vonf1wev  35956  vonf1owevOLD  35958  onprcf1acwevdlem1  35965  vsmrep  36010  axrepprim  36560  axunprim  36561  axpowprim  36562  axinfprim  36564  axacprim  36565  untuni  36567  elintfv  36623  dfon2lem8  36645  dfon2lem9  36646  19.12b  36656  brtxpsd3  36751  dfom5b  36767  dffun10  36769  disjeq1i  37074  ss-ax8  37107  cbvdisjvw2  37117  mh-setind  37417  regsfromregtco  37419  regsfromsetind  37420  regsfromunir1  37421  mh-prprimbi  37424  mh-unprimbi  37425  mh-infprim1bi  37427  mh-infprim2bi  37428  mh-infprim3bi  37429  bj-notalbii  37592  bj-cbvaew  37636  bj-ssbeq  37645  bj-ax12ssb  37650  bj-nfalt  37708  bj-substax12  37719  bj-nnfalt  37785  bj-nnfext  37786  ax11-pm2  37841  bj-sblem  37849  eliminable-veqab  37871  eliminable-abeqv  37872  eliminable-abeqab  37873  bj-ralvw  37884  bj-sbeq  37906  bj-nfcf  37928  bj-snsetex  37969  bj-rcleqf  38031  bj-clex  38037  bj-rep  38082  bj-axseprep  38083  fvineqsneq  38429  wl-equsalvw  38564  wl-equsalcom  38569  wl-sb9v  38575  wl-sb8eft  38577  wl-sb8et  38579  wl-2sb6d  38584  wl-alanbii  38595  wl-sb8eut  38604  wl-sb8eutv  38605  poimirlem25  38657  poimirlem30  38662  heibor1lem  38837  sbcalfi  39142  mpobi123f  39188  mptbi12f  39192  ineccnvmo  39383  alrmomorn  39384  ralmo  39386  ralrmo3  39390  cocossss  39552  cossssid3  39585  cossssid4  39586  cosscnvssid4  39593  trcoss2  39600  dfeldisj4  39838  dfeldisj5  39839  disjres  39870  dvelimf-o  40080  axc11n-16  40089  pmapglbx  40920  sn-axrep5v  43365  abbibw  43782  dford4  44130  unielss  44314  onsupmaxb  44335  rp-fakeinunass  44610  rababg  44669  elmapintrab  44671  elinintrab  44672  undmrnresiss  44698  clss2lem  44705  cotrintab  44708  elintima  44747  relexp0eq  44795  dfhe3  44869  snhesn  44880  psshepw  44882  dffrege76  45033  frege77  45034  frege110  45067  dffrege115  45072  frege116  45073  frege118  45075  frege131  45088  ntrneikb  45188  ismnuprim  45372  rr-grothprimbi  45373  ismnushort  45379  rr-grothshortbi  45381  pm10.541  45445  pm10.542  45446  19.21vv  45454  19.31vv  45462  19.28vv  45464  pm11.62  45472  axc11next  45484  pm13.196a  45492  2sbc6g  45493  elnev  45515  hbexgVD  45982  dfac5prim  46074  permaxext  46089  permaxrep  46090  permaxpow  46093  permac8prim  46098  rabssf  46228  sinnpoly  48035  2rexsb  48265  dfich2  48634  ichal  48642  spr0nelg  48652  mo0sn  50021  setis  50960  alimp-surprise  51045  alimp-no-surprise  51046  dfrals2  51055  alsbii  51065  dfralseu2  51088  alseubii  51097  dfalseu2  51101