Theorem albii 1852

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

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

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

This proof depends on definitions:  df-bi 210

This theorem is used by:  2albii  1853  3albii  1854  hbxfrbi  1858  alex  1859  2nalexn  1861  2exnaln  1862  imnang  1875  alexn  1878  19.26-2  1904  19.26-3an  1905  19.43OLD  1916  albiim  1922  2albiim  1923  empty  1939  19.32v  1973  19.31v  1974  19.23vv  1976  pm11.53v  1977  19.12vvv  2027  equsalvw  2037  2sb6  2123  sbrimvwOLD  2129  sbbiiev  2130  alrot3  2198  alrot4  2199  sbal  2207  sbalv  2208  19.21-2  2248  19.32  2272  19.31  2273  equsalv  2305  sbn  2317  sbrim  2341  aaan  2367  pm11.53  2380  19.12vv  2381  sb8v  2387  sb8f  2388  cbvsbvf  2397  equsal  2451  2sb6rf  2507  sbcom3  2540  sb8eulem  2628  eu1  2640  2mo2  2677  2eu1  2680  2eu1v  2681  2eu3  2683  euae  2689  nulmo  2742  eqabbw  2838  eqabcbw  2839  hblem  2896  hblemg  2897  eqabcb  2905  nfceqi  2924  eqabf  2956  ralbii2  3109  r2allem  3155  r3al  3205  r19.21t  3261  r19.23t  3263  ralcom4  3293  cbvralsvw  3318  sbralie  3344  sbralieOLD  3346  rabbi  3448  rabid2f  3449  rabid2im  3450  eqv  3467  eqvf  3468  abv  3469  abvALT  3470  ralv  3483  ceqsralt  3491  ceqsal  3494  ceqsalv  3496  rspc2gv  3593  ralxpxfr2d  3607  clel2g  3620  clel4g  3624  ralab  3658  ralrab2  3663  euind  3689  reu2  3690  reu3  3692  rmo4  3695  reu8  3698  rmo3f  3699  rmoim  3705  2reuswap  3711  2reuswap2  3712  reuind  3718  2reu5lem2  3721  2reu5lem3  3722  2rmoswap  3726  sbccomlem  3824  rmo2  3841  rmo3  3843  rmoanim  3849  dfss2  3924  ss2ab  4016  ss2rab  4024  rabss  4025  ss2rabd  4027  uniiunlem  4042  ssequn1  4139  unss  4143  ralunb  4150  ssin  4191  eq0f  4301  eq0  4304  eq0ALT  4305  ssdif0  4321  inssdif0OLD  4330  ab0w  4335  ab0  4336  ab0ALT  4337  ab0orv  4339  disj  4410  disj3  4414  ssundif  4450  ralf0  4460  ralidmw  4479  ralidm  4480  pwss  4588  rabsssn  4636  rabeqsnd  4637  ralsnsg  4638  ralsng  4643  disjsn  4679  snssb  4750  pwpw0  4781  dfnfc2  4896  unissb  4908  elintrab  4927  ssintrab  4938  intun  4947  intprg  4948  dfiin2g  4997  iunssf  5009  iunssfOLD  5010  iunss  5011  iunssOLD  5012  dfdisj2  5080  cbvdisj  5088  cbvdisjv  5089  disjor  5093  dftr2  5222  dftr5  5224  axrep1  5241  axrep4v  5245  axrep4  5246  axrep5  5248  axrep6  5249  axrep6OLD  5250  zfrep6  5252  axsepgfromrep  5257  axnulALT  5269  vnexOLD  5283  inex1  5288  axpweq  5323  zfpow  5339  axpow2  5340  nfnid  5348  dtruALT  5361  reusv2lem4  5374  zfpair2  5407  prex  5411  el.OLD  5422  ssextss  5436  moabexOLD  5442  dffr6  5619  dffr2  5624  dffr2ALT  5625  dfepfr  5647  frinxp  5746  ssrel2  5773  eqrelrel  5785  raliunxp  5827  relop  5838  dmopab3  5911  dm0rn0  5916  dm0rn0OLD  5917  reldm0  5920  rnopab3  5948  iresn0n0  6058  dffr3  6103  cotrg  6113  idrefALT  6115  asymref  6118  asymref2  6119  intirr  6120  dffr4  6325  sucel  6441  sb8iota  6507  dffun6  6551  dffun3  6552  dffun4  6553  dffun5  6554  dffun6f  6555  dffun7  6567  funopab  6575  funcnv2  6608  funcnv  6609  fun2cnv  6611  fun11  6614  fununi  6615  fnres  6666  mptfnf  6674  fnopabg  6676  tz6.12-2  6872  brprcneu  6875  brprcneuALT  6876  dffv2  6980  funcnvmpt  6995  fvn0ssdmfun  7073  dff13  7254  fnssintima  7368  eqoprab2bw  7486  eqoprab2b  7487  mpo2eqb  7548  ralrnmpo  7555  imaeqalov  7655  zfun  7739  uniex2  7741  uniex2OLD  7742  funcnvuni  7931  ralxp3f  8135  frpoins3xpg  8138  frpoins3xp3g  8139  xpord3inddlem  8152  dfer2  8697  fiint  9289  marypha1lem  9396  marypha2lem3  9400  inf2  9595  axinf2  9612  ttrclss  9692  scottexsOLD  9875  scott0bsOLD  9877  aceq1  10113  dfac4  10118  dfac7  10128  dfac0  10129  dfac1  10130  dfac10  10133  dfac10c  10134  dfac10b  10135  kmlem4  10149  kmlem12  10157  kmlem14  10159  kmlem15  10160  kmlem16  10161  dfackm  10162  ac6n  10480  axpowndlem3  10595  zfcndrep  10610  zfcndun  10611  zfcndpow  10612  axgroth5  10820  axgroth2  10821  axgroth4  10828  grothprim  10830  sstskm  10838  fimaxre3  12172  infm3  12185  nnwos  12950  cotr2g  15032  brtrclfv  15058  trclfvcotr  15065  rpnnen2lem12  16298  isprm2  16757  vdwmc2  17056  pgpfac1  20175  pgpfac  20179  ssdifidlprm  21515  iunocv  21860  2ndcdisj2  23643  hausdiag  23831  rnelfmlem  24138  alexsubALTlem3  24235  cnextfun  24250  itg2leub  25922  eqcuts2  28008  addsuniflem  28223  mulsuniflem  28371  onsfi  28578  mpteleeOLD  29274  nmoubi  31153  nmobndseqi  31160  nmobndseqiALT  31161  isch2  31604  isch3  31622  choc0  31707  nmopub  32289  nmfnleub  32306  xfree2  32826  mo5f  32864  nmo  32865  reuxfrdf  32866  rabsspr  32876  rabsstp  32877  inpr0  32907  cbvdisjf  32945  disjorf  32953  ssrelf  32989  funcnv5mpt  33041  ballotlem2  34903  bnj89  35134  bnj115  35138  bnj1143  35202  bnj110  35270  bnj611  35330  bnj864  35334  bnj865  35335  bnj1000  35353  bnj978  35361  bnj1049  35386  bnj1052  35387  bnj1090  35391  bnj1030  35399  bnj1133  35401  bnj1171  35412  bnj1172  35413  bnj1174  35415  bnj1176  35417  bnj1204  35424  bnj1253  35429  bnj1388  35445  bnj1523  35483  axnulALT2  35493  fineqvrep  35543  fineqvpow  35544  axreg  35556  axregscl  35557  axregs  35568  axpowg  35575  vonf1wev  35608  vonf1owevOLD  35610  axrepprim  36207  axunprim  36208  axpowprim  36209  axinfprim  36211  axacprim  36212  untuni  36214  dffr5  36259  elintfv  36270  dfon2lem8  36293  dfon2lem9  36294  19.12b  36304  brtxpsd3  36399  dfom5b  36415  dffun10  36417  disjeq1i  36737  ss-ax8  36770  cbvdisjvw2  36780  mh-setind  37080  regsfromregtco  37082  regsfromsetind  37083  regsfromunir1  37084  mh-prprimbi  37087  mh-unprimbi  37088  mh-infprim1bi  37090  mh-infprim2bi  37091  mh-infprim3bi  37092  bj-notalbii  37255  bj-cbvaew  37299  bj-ssbeq  37308  bj-ax12ssb  37313  bj-nfalt  37371  bj-substax12  37382  bj-nnfalt  37448  bj-nnfext  37449  ax11-pm2  37504  bj-sblem  37512  eliminable-veqab  37534  eliminable-abeqv  37535  eliminable-abeqab  37536  bj-ralvw  37547  bj-sbeq  37569  bj-nfcf  37591  bj-snsetex  37632  bj-rcleqf  37694  bj-clex  37700  bj-rep  37743  bj-axseprep  37744  fvineqsneq  38091  wl-equsalvw  38226  wl-equsalcom  38231  wl-sb9v  38237  wl-sb8eft  38239  wl-sb8et  38241  wl-2sb6d  38246  wl-alanbii  38257  wl-sb8eut  38266  wl-sb8eutv  38267  poimirlem25  38329  poimirlem30  38334  heibor1lem  38493  sbcalfi  38798  mpobi123f  38844  mptbi12f  38848  ineccnvmo  39039  alrmomorn  39040  ralmo  39042  ralrmo3  39046  cocossss  39208  cossssid3  39241  cossssid4  39242  cosscnvssid4  39249  trcoss2  39256  dfeldisj4  39494  dfeldisj5  39495  disjres  39526  dvelimf-o  39736  axc11n-16  39745  pmapglbx  40576  sn-axrep5v  43021  abbibw  43442  dford4  43789  unielss  43978  onsupmaxb  43999  rp-fakeinunass  44274  rababg  44333  elmapintrab  44335  elinintrab  44336  undmrnresiss  44363  clss2lem  44370  cotrintab  44373  elintima  44412  relexp0eq  44460  dfhe3  44534  snhesn  44545  psshepw  44547  dffrege76  44698  frege77  44699  frege110  44732  dffrege115  44737  frege116  44738  frege118  44740  frege131  44753  ntrneikb  44853  ismnuprim  45037  rr-grothprimbi  45038  ismnushort  45044  rr-grothshortbi  45046  pm10.541  45110  pm10.542  45111  19.21vv  45119  19.31vv  45127  19.28vv  45129  pm11.62  45137  axc11next  45149  pm13.196a  45157  2sbc6g  45158  elnev  45180  hbexgVD  45647  dfac5prim  45732  permaxext  45747  permaxrep  45748  permaxpow  45751  permac8prim  45756  rabssf  45870  sinnpoly  47661  2rexsb  47871  dfich2  48240  ichal  48248  spr0nelg  48258  mo0sn  49627  dffun3f  50493  setrec1lem2  50499  setrec2  50506  setis  50509  alimp-surprise  50591  alimp-no-surprise  50592  dfrals2  50601  alsbii  50611  dfralseu2  50634  alseubii  50643  dfalseu2  50647