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  1918  albiim  1924  2albiim  1925  empty  1941  19.32v  1975  19.31v  1976  19.23vv  1978  pm11.53v  1979  19.12vvv  2029  equsalvw  2039  2sb6  2125  sbrimvwOLD  2131  sbbiiev  2132  alrot3  2200  alrot4  2201  sbal  2209  sbalv  2210  19.21-2  2249  19.32  2273  19.31  2274  equsalv  2305  sbn  2317  sbrim  2341  aaan  2366  pm11.53  2379  19.12vv  2380  sb8v  2385  sb8f  2386  cbvsbvf  2395  equsal  2449  2sb6rf  2505  sbcom3  2538  sb8eulem  2626  eu1  2638  2mo2  2675  2eu1  2678  2eu1v  2679  2eu3  2681  euae  2687  nulmo  2740  abbib  2832  eqabbw  2837  eqabcbw  2838  hblem  2895  hblemg  2896  eqabcb  2904  nfceqi  2923  eqabf  2955  ralbii2  3108  r2allem  3154  r3al  3204  r19.21t  3260  r19.23t  3262  ralcom4  3292  cbvralsvw  3317  sbralie  3342  sbralieOLD  3344  rabbi  3445  rabid2f  3446  rabid2im  3447  eqv  3464  eqvf  3465  abv  3466  abvALT  3467  ralv  3480  ceqsralt  3488  ceqsal  3491  ceqsalv  3493  rspc2gv  3589  ralxpxfr2d  3603  clel2g  3616  clel4g  3620  ralab  3654  ralrab2  3659  euind  3685  reu2  3686  reu3  3688  rmo4  3691  reu8  3694  rmo3f  3695  rmoim  3701  2reuswap  3707  2reuswap2  3708  reuind  3714  2reu5lem2  3717  2reu5lem3  3718  2rmoswap  3722  sbccomlem  3821  rmo2  3838  rmo3  3840  rmoanim  3846  ss2ab  3989  ss2rab  3997  rabss  3998  ss2rabd  4000  uniiunlem  4015  dfss2  4097  ssin  4138  ssequn1  4187  unss  4191  ralunb  4198  eq0f  4297  eq0  4300  eq0ALT  4301  ssdif0  4317  inssdif0OLD  4326  ab0w  4331  ab0  4332  ab0ALT  4333  ab0orv  4335  disj  4406  disj3  4410  ssundif  4446  ralf0  4456  ralidmw  4475  ralidm  4476  pwss  4585  rabsssn  4629  rabeqsnd  4630  ralsnsg  4631  ralsng  4636  disjsn  4672  snssb  4743  pwpw0  4834  dfnfc2  4892  unissb  4904  elintrab  4923  ssintrab  4934  intun  4943  intprg  4944  dfiin2g  4992  iunssf  5004  iunssfOLD  5005  iunss  5006  iunssOLD  5007  dfdisj2  5075  cbvdisj  5083  cbvdisjv  5084  disjor  5088  dftr2  5218  dftr5  5220  axrep1  5237  axrep4v  5241  axrep4  5242  axrep5  5243  axrep6  5244  zfrep6  5246  axsepgfromrep  5251  axnulALT  5262  vnexOLD  5276  inex1  5282  axpweq  5317  zfpow  5333  axpow2  5334  nfnid  5342  dtruALT  5355  reusv2lem4  5368  zfpair2  5397  prex  5401  el.OLD  5412  ssextss  5426  moabexOLD  5432  dffr6  5612  dffr2  5617  dffr2ALT  5618  dfepfr  5640  frinxp  5740  ssrel2  5768  eqrelrel  5780  raliunxp  5824  relop  5836  dmopab3  5911  dm0rn0  5916  dm0rn0OLD  5917  reldm0  5920  rnopab3  5948  iresn0n0  6062  dffr3  6113  cotrg  6121  idrefALT  6123  asymref  6126  asymref2  6127  intirr  6128  dffr4  6347  sucel  6463  sb8iota  6529  dffun6  6575  dffun3  6576  dffun4  6577  dffun5  6578  dffun6f  6579  dffun7  6593  funopab  6601  funcnv2  6636  funcnv  6637  fun2cnv  6639  fun11  6642  fununi  6643  fnres  6694  mptfnf  6702  fnopabg  6704  tz6.12-2  6901  brprcneu  6904  brprcneuALT  6905  dffv2  7009  funcnvmpt  7024  fvn0ssdmfun  7104  dff13  7287  fnssintima  7401  eqoprab2bw  7519  eqoprab2b  7520  mpo2eqb  7581  ralrnmpo  7589  imaeqalov  7690  zfun  7782  uniex2  7784  uniex2OLD  7785  funcnvuni  7976  ralxp3f  8189  frpoins3xpg  8192  frpoins3xp3g  8193  xpord3inddlem  8206  dfer2  8754  fiint  9354  marypha1lem  9460  marypha2lem3  9464  inf2  9659  axinf2  9676  ttrclss  9756  scottexsOLD  9978  scott0bsOLD  9980  setrec1lem2  10002  dffun3f  10010  setrec2  10012  aceq1  10233  dfac4  10238  dfac7  10248  dfac0  10249  dfac1  10250  dfac10  10253  dfac10c  10254  dfac10b  10255  kmlem4  10269  kmlem12  10277  kmlem14  10279  kmlem15  10280  kmlem16  10281  dfackm  10282  ac6n  10600  axpowndlem3  10721  zfcndrep  10736  zfcndun  10737  zfcndpow  10738  axgroth5  10946  axgroth2  10947  axgroth4  10954  grothprim  10956  sstskm  10964  fimaxre3  12301  infm3  12314  nnwos  13080  cotr2g  15170  brtrclfv  15196  trclfvcotr  15203  rpnnen2lem12  16434  isprm2  16898  vdwmc2  17198  pgpfac1  20338  pgpfac  20342  ssdifidlprm  21684  iunocv  22031  2ndcdisj2  23820  hausdiag  24008  rnelfmlem  24315  alexsubALTlem3  24412  cnextfun  24427  itg2leub  26099  eqcuts2  28218  addsuniflem  28433  mulsuniflem  28581  onsfi  28788  mpteleeOLD  29519  nmoubi  31420  nmobndseqi  31427  nmobndseqiALT  31428  isch2  31871  isch3  31889  choc0  31974  nmopub  32556  nmfnleub  32573  xfree2  33135  mo5f  33173  nmo  33174  reuxfrdf  33175  rabsspr  33185  rabsstp  33186  inpr0  33216  cbvdisjf  33253  disjorf  33261  ssrelf  33297  funcnv5mpt  33349  ballotlem2  35225  bnj89  35456  bnj115  35460  bnj1143  35524  bnj110  35592  bnj611  35652  bnj864  35656  bnj865  35657  bnj1000  35675  bnj978  35683  bnj1049  35708  bnj1052  35709  bnj1090  35713  bnj1030  35721  bnj1133  35723  bnj1171  35734  bnj1172  35735  bnj1174  35737  bnj1176  35739  bnj1204  35746  bnj1253  35751  bnj1388  35767  bnj1523  35805  axnulALT2  35818  fineqvrep  35916  fineqvpow  35917  axreg  35929  axregscl  35930  axregs  35941  axpowg  35948  vonf1wev  36070  vonf1owevOLD  36072  onprcf1acwevdlem1  36079  vsmrep  36124  mirimanofffr  36663  axrepprim  36675  axunprim  36676  axpowprim  36677  axinfprim  36679  axacprim  36680  untuni  36682  elintfv  36738  dfon2lem8  36760  dfon2lem9  36761  19.12b  36771  brtxpsd3  36866  dfom5b  36882  dffun10  36884  disjeq1i  37189  ss-ax8  37222  cbvdisjvw2  37232  mh-setind  37532  regsfromregtco  37534  regsfromsetind  37535  regsfromunir1  37536  mh-prprimbi  37539  mh-unprimbi  37540  mh-infprim1bi  37542  mh-infprim2bi  37543  mh-infprim3bi  37544  bj-notalbii  37707  bj-cbvaew  37751  bj-ssbeq  37760  bj-ax12ssb  37765  bj-nfalt  37823  bj-substax12  37834  bj-nnfalt  37900  bj-nnfext  37901  ax11-pm2  37956  bj-sblem  37964  eliminable-veqab  37986  eliminable-abeqv  37987  eliminable-abeqab  37988  bj-ralvw  37999  bj-sbeq  38021  bj-nfcf  38043  bj-snsetex  38084  bj-rcleqf  38146  bj-clex  38152  bj-rep  38252  bj-axseprep  38253  fvineqsneq  38596  wl-equsalvw  38731  wl-equsalcom  38736  wl-sb9v  38742  wl-sb8eft  38744  wl-sb8et  38746  wl-2sb6d  38751  wl-alanbii  38762  wl-sb8eut  38771  wl-sb8eutv  38772  poimirlem25  38824  poimirlem30  38829  heibor1lem  39002  sbcalfi  39307  mpobi123f  39353  mptbi12f  39357  ineccnvmo  39548  alrmomorn  39549  ralmo  39551  ralrmo3  39555  cocossss  39717  cossssid3  39750  cossssid4  39751  cosscnvssid4  39758  trcoss2  39765  dfeldisj4  40003  dfeldisj5  40004  disjres  40035  dvelimf-o  40245  axc11n-16  40254  pmapglbx  41085  sn-axrep5v  43531  abbibw  43948  dford4  44296  unielss  44475  onsupmaxb  44496  rp-fakeinunass  44771  rababg  44830  elmapintrab  44832  elinintrab  44833  undmrnresiss  44859  clss2lem  44866  cotrintab  44869  elintima  44908  relexp0eq  44956  dfhe3  45030  snhesn  45041  psshepw  45043  dffrege76  45194  frege77  45195  frege110  45228  dffrege115  45233  frege116  45234  frege118  45236  frege131  45249  ntrneikb  45349  ismnuprim  45533  rr-grothprimbi  45534  ismnushort  45540  rr-grothshortbi  45542  pm10.541  45606  pm10.542  45607  19.21vv  45615  19.31vv  45623  19.28vv  45625  pm11.62  45633  axc11next  45645  pm13.196a  45653  2sbc6g  45654  elnev  45675  hbexgVD  46142  dfac5prim  46238  permaxext  46253  permaxrep  46254  permaxpow  46257  permac8prim  46262  rabssf  46401  sinnpoly  48208  2rexsb  48439  dfich2  48807  ichal  48815  spr0nelg  48825  mo0sn  50252  setis  51191  alimp-surprise  51298  alimp-no-surprise  51299  dfrals2  51308  alsbii  51318  dfralseu2  51341  alseubii  51350  dfalseu2  51354