Theorem albii 1822

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

Syntax hints:   ↔ wb 205  ∀wal 1537

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

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  2albii  1823  3albii  1824  hbxfrbi  1828  alex  1829  2nalexn  1831  2exnaln  1832  imnang  1845  alexn  1848  nfnbiOLD  1859  19.26-2  1875  19.26-3an  1876  19.43OLD  1887  albiim  1893  2albiim  1894  empty  1910  19.32v  1944  19.31v  1945  19.23vv  1947  pm11.53v  1948  19.12vvv  1993  equsalvw  2008  2sb6  2090  sbrimvw  2095  sbcom3vv  2099  alrot3  2158  alrot4  2159  sbal  2160  sbalv  2161  19.21-2  2203  19.32  2227  19.31  2228  equsalv  2260  sbn  2278  sbrim  2302  aaan  2329  aaanOLD  2330  pm11.53  2345  19.12vv  2346  sb8v  2351  sb8f  2352  sbievg  2362  equsal  2418  2sb6rf  2474  sbcom3  2511  sb8eulem  2599  eu1  2613  2mo2  2650  2eu1  2653  2eu1v  2654  2eu3  2656  euae  2662  nulmo  2715  abeq2w  2816  hblem  2871  hblemg  2872  abeq2  2873  abeq1  2874  abbiOLD  2881  nfcriOLD  2898  nfcriOLDOLD  2899  nfcriiOLD  2901  nfceqi  2905  abeq2f  2941  ralbii2  3091  r19.21vOLD  3115  r2allem  3118  r3al  3120  r19.21t  3140  nfra2wOLD  3156  ralcom4  3165  ralcom4OLD  3166  r19.23t  3247  rabid2f  3314  rabid2OLD  3316  rabbi  3317  moel  3359  moelOLD  3360  eqv  3442  eqvf  3443  abv  3444  abvALT  3445  ralv  3457  ceqsralt  3464  ceqsalv  3468  rspc2gv  3570  ralxpxfr2d  3577  clel2g  3589  clel4g  3594  elabgt  3604  elabg  3608  ralab  3629  ralabOLD  3630  ralrab2  3636  euind  3660  reu2  3661  reu3  3663  rmo4  3666  reu8  3669  rmo3f  3670  rmoim  3676  2reuswap  3682  2reuswap2  3683  reuind  3689  2reu5lem2  3692  2reu5lem3  3693  2rmoswap  3697  rmo2  3821  rmo3  3823  rmoanim  3828  dfss2  3908  dfss2OLD  3909  ss2ab  3994  ss2rab  4005  rabss  4006  uniiunlem  4020  dfdif3  4050  ssequn1  4115  unss  4119  ralunb  4126  ssin  4165  vn0  4273  eq0f  4275  eq0  4278  eq0ALT  4279  ssdif0  4298  inssdif0  4304  ab0w  4308  ab0  4309  ab0OLD  4310  ab0ALT  4311  ab0orv  4313  eq0rdv  4339  disj  4382  disjOLD  4383  disj3  4388  ssundif  4419  ralidmw  4439  ralidm  4443  ralf0  4445  ralf0OLD  4449  pwss  4559  rabsssn  4604  ralsnsg  4605  ralsng  4610  disjsn  4648  snssg  4719  pwpw0  4747  pwsnOLD  4833  dfnfc2  4864  unissb  4874  elintrab  4892  ssintrab  4903  intun  4912  intprg  4913  intprOLD  4915  dfiin2g  4963  iunssf  4975  iunss  4976  dfdisj2  5042  cbvdisj  5050  disjor  5055  dftr2  5194  dftr5  5195  axrep1  5211  axrep5  5216  axrep6  5217  axsepgfromrep  5222  axnulALT  5229  vnex  5239  inex1  5242  axpweq  5288  zfpow  5290  axpow2  5291  axpow3  5292  nfnid  5299  dtruALT  5312  reusv2lem4  5325  zfpair2  5354  el  5358  ssextss  5370  moabex  5375  dffr6  5548  dffr2  5554  dffr2ALT  5555  dfepfr  5575  frinxp  5670  ssrel2  5697  eqrelrel  5709  reliun  5728  raliunxp  5751  relop  5762  dmopab3  5831  dm0rn0  5837  reldm0  5840  iresn0n0  5966  dffr3  6010  cotrg  6020  cotrgOLD  6021  idrefALT  6023  asymref  6026  asymref2  6027  intirr  6028  dffr4  6226  sucel  6343  sb8iota  6407  dffun2OLD  6448  dffun6  6449  dffun3  6450  dffun3OLD  6451  dffun4  6452  dffun5  6453  dffun6f  6454  dffun7  6468  funopab  6476  funcnv2  6509  funcnv  6510  fun2cnv  6512  fun11  6515  fununi  6516  fnres  6568  mptfnf  6577  fnopabg  6579  brprcneu  6773  brprcneuALT  6774  dffv2  6872  fvn0ssdmfun  6961  dff13  7137  eqoprab2bw  7354  eqoprab2b  7355  mpo2eqb  7415  ralrnmpo  7421  zfun  7598  uniex2  7600  funcnvuni  7787  dfer2  8508  fiint  9100  marypha1lem  9201  marypha2lem3  9205  inf2  9390  axinf2  9407  ttrclss  9487  scottexs  9654  scott0s  9655  aceq1  9882  dfac4  9887  dfac7  9897  dfac0  9898  dfac1  9899  dfac10  9902  dfac10c  9903  dfac10b  9904  kmlem4  9918  kmlem12  9926  kmlem14  9928  kmlem15  9929  kmlem16  9930  dfackm  9931  ac6n  10250  axpowndlem3  10364  zfcndrep  10379  zfcndun  10380  zfcndpow  10381  axgroth5  10589  axgroth2  10590  axgroth4  10597  grothprim  10599  sstskm  10607  fimaxre3  11930  infm3  11943  nnwos  12664  cotr2g  14696  brtrclfv  14722  trclfvcotr  14729  rpnnen2lem12  15943  isprm2  16396  vdwmc2  16689  pgpfac1  19692  pgpfac  19696  iunocv  20895  2ndcdisj2  22617  hausdiag  22805  rnelfmlem  23112  alexsubALTlem3  23209  cnextfun  23224  itg2leub  24908  mptelee  27272  nmoubi  29143  nmobndseqi  29150  nmobndseqiALT  29151  isch2  29594  isch3  29612  choc0  29697  nmopub  30279  nmfnleub  30296  xfree2  30816  nelbOLDOLD  30826  mo5f  30846  nmo  30847  reuxfrdf  30848  rabeqsnd  30857  inpr0  30889  cbvdisjf  30919  disjorf  30927  ssrelf  30964  funcnvmpt  31013  funcnv5mpt  31014  ballotlem2  32464  bnj89  32709  bnj115  32713  bnj1143  32779  bnj110  32847  bnj611  32907  bnj864  32911  bnj865  32912  bnj1000  32930  bnj978  32938  bnj1049  32963  bnj1052  32964  bnj1090  32968  bnj1030  32976  bnj1133  32978  bnj1171  32989  bnj1172  32990  bnj1174  32992  bnj1176  32994  bnj1204  33001  bnj1253  33006  bnj1388  33022  bnj1523  33060  fineqvrep  33073  fineqvpow  33074  axrepprim  33652  axunprim  33653  axpowprim  33654  axinfprim  33656  axacprim  33657  untuni  33659  fnssintima  33685  ralxp3f  33694  dffr5  33730  elintfv  33747  dfon2lem8  33775  dfon2lem9  33776  19.12b  33786  frpoins3xpg  33796  frpoins3xp3g  33797  eqscut2  34009  brtxpsd3  34207  dfom5b  34223  dffun10  34225  bj-notalbii  34805  bj-ssbeq  34843  bj-ax12ssb  34848  bj-hbext  34901  bj-nfalt  34902  bj-substax12  34912  bj-nnfalt  34957  bj-nnfext  34958  ax11-pm2  35028  bj-sbnf  35033  bj-sblem  35037  eliminable-veqab  35059  eliminable-abeqv  35060  eliminable-abeqab  35061  bj-ralvw  35073  bj-sbeq  35095  bj-nfcf  35120  bj-snsetex  35162  bj-rcleqf  35224  fvineqsneq  35592  wl-equsalvw  35706  wl-equsalcom  35710  wl-sb8et  35717  wl-2sb6d  35722  wl-alanbii  35733  wl-sb8eut  35741  poimirlem25  35811  poimirlem30  35816  heibor1lem  35976  sbcalfi  36283  mpobi123f  36329  mptbi12f  36333  ineccnvmo  36496  alrmomorn  36497  cocossss  36566  cossssid3  36594  cossssid4  36595  cosscnvssid4  36602  trcoss2  36609  dfeldisj4  36838  dfeldisj5  36839  dvelimf-o  36950  axc11n-16  36959  pmapglbx  37790  sn-axrep5v  40192  dford4  40858  rp-fakeinunass  41129  rababg  41188  elmapintrab  41191  elinintrab  41192  undmrnresiss  41219  clss2lem  41226  cotrintab  41229  elintima  41268  ss2iundf  41274  relexp0eq  41316  dfhe3  41390  snhesn  41401  psshepw  41403  dffrege76  41554  frege77  41555  frege110  41588  dffrege115  41593  frege116  41594  frege118  41596  frege131  41609  ntrneikb  41711  ismnuprim  41919  rr-grothprimbi  41920  ismnushort  41926  rr-grothshortbi  41928  pm10.541  41992  pm10.542  41993  19.21vv  42001  19.31vv  42009  19.28vv  42011  pm11.62  42019  axc11next  42031  pm13.196a  42039  2sbc6g  42040  elnev  42063  hbexgVD  42533  rabssf  42675  2rexsb  44604  dfich2  44921  ichal  44929  spr0nelg  44939  mo0sn  46172  dffun3f  46399  setrec1lem2  46405  setrec2  46412  setis  46414  alimp-surprise  46495  alimp-no-surprise  46496