Theorem albii 1819

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

Syntax hints:   ↔ wb 206  ∀wal 1538

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

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  2albii  1820  3albii  1821  hbxfrbi  1825  alex  1826  2nalexn  1828  2exnaln  1829  imnang  1842  alexn  1845  19.26-2  1871  19.26-3an  1872  19.43OLD  1883  albiim  1889  2albiim  1890  empty  1906  19.32v  1940  19.31v  1941  19.23vv  1943  pm11.53v  1944  19.12vvv  1994  equsalvw  2004  2sb6  2087  sbrimvw  2092  sbbiiev  2093  alrot3  2161  alrot4  2162  sbal  2170  sbalv  2171  19.21-2  2210  19.32  2234  19.31  2235  equsalv  2268  sbn  2280  sbrim  2304  sbnfOLD  2312  aaan  2331  pm11.53  2344  19.12vv  2345  sb8v  2351  sb8f  2352  cbvsbvf  2362  equsal  2416  2sb6rf  2472  sbcom3  2505  sb8eulem  2592  eu1  2604  2mo2  2641  2eu1  2645  2eu1v  2646  2eu3  2648  euae  2654  nulmo  2707  eqabbw  2803  hblem  2860  hblemg  2861  eqabbOLD  2869  eqabcb  2870  nfceqi  2889  eqabf  2922  ralbii2  3072  r2allem  3122  r19.21vOLD  3160  r3al  3176  r19.21t  3232  r19.23t  3234  ralcom4  3264  cbvralsvw  3292  sbralie  3328  sbralieOLD  3330  rabbi  3439  rabid2f  3440  rabid2im  3441  eqv  3460  eqvf  3461  abv  3462  abvALT  3463  ralv  3477  ceqsralt  3485  ceqsal  3488  ceqsalv  3490  rspc2gv  3601  ralxpxfr2d  3615  clel2g  3628  clel4g  3632  elabgtOLDOLD  3643  ralab  3667  ralrab2  3672  euind  3698  reu2  3699  reu3  3701  rmo4  3704  reu8  3707  rmo3f  3708  rmoim  3714  2reuswap  3720  2reuswap2  3721  reuind  3727  2reu5lem2  3730  2reu5lem3  3731  2rmoswap  3735  sbccomlem  3835  rmo2  3853  rmo3  3855  rmoanim  3860  dfss2  3935  ss2ab  4028  ss2rab  4037  rabss  4038  uniiunlem  4053  dfdif3OLD  4084  ssequn1  4152  unss  4156  ralunb  4163  ssin  4205  vn0  4311  eq0f  4313  eq0  4316  eq0ALT  4317  ssdif0  4332  inssdif0  4340  ab0w  4345  ab0  4346  ab0ALT  4347  ab0orv  4349  eq0rdv  4373  disj  4416  disj3  4420  ssundif  4454  ralidmw  4474  ralidm  4478  ralf0  4480  pwss  4589  rabsssn  4635  rabeqsnd  4636  ralsnsg  4637  ralsng  4642  disjsn  4678  snssb  4749  snssgOLD  4751  pwpw0  4780  dfnfc2  4896  unissb  4906  unissbOLD  4907  elintrab  4927  ssintrab  4938  intun  4947  intprg  4948  dfiin2g  4999  iunssf  5011  iunss  5012  dfdisj2  5079  cbvdisj  5087  cbvdisjv  5088  disjor  5092  dftr2  5219  dftr5  5221  dftr5OLD  5222  axrep1  5238  axrep4v  5242  axrep4  5243  axrep5  5245  axrep6  5246  axrep6OLD  5247  axsepgfromrep  5252  axnulALT  5262  vnex  5272  inex1  5275  axpweq  5309  zfpow  5324  axpow2  5325  nfnid  5333  dtruALT  5346  reusv2lem4  5359  zfpair2  5391  el  5400  ssextss  5416  moabex  5422  dffr6  5597  dffr2  5602  dffr2ALT  5603  dfepfr  5625  frinxp  5724  ssrel2  5751  eqrelrel  5763  reliun  5782  raliunxp  5806  relop  5817  dmopab3  5886  dm0rn0  5891  reldm0  5894  rnopab3  5923  iresn0n0  6028  dffr3  6073  cotrg  6083  cotrgOLD  6084  cotrgOLDOLD  6085  idrefALT  6087  asymref  6092  asymref2  6093  intirr  6094  dffr4  6296  sucel  6411  sb8iota  6478  dffun2OLDOLD  6526  dffun6  6527  dffun3  6528  dffun3OLD  6529  dffun4  6530  dffun5  6531  dffun6f  6532  dffun7  6546  funopab  6554  funcnv2  6587  funcnv  6588  fun2cnv  6590  fun11  6593  fununi  6594  fnres  6648  mptfnf  6656  fnopabg  6658  brprcneu  6851  brprcneuALT  6852  dffv2  6959  fvn0ssdmfun  7049  dff13  7232  fnssintima  7340  eqoprab2bw  7462  eqoprab2b  7463  mpo2eqb  7524  ralrnmpo  7531  imaeqalov  7631  zfun  7715  uniex2  7717  funcnvuni  7911  ralxp3f  8119  frpoins3xpg  8122  frpoins3xp3g  8123  xpord3inddlem  8136  dfer2  8675  fiint  9284  fiintOLD  9285  marypha1lem  9391  marypha2lem3  9395  inf2  9583  axinf2  9600  ttrclss  9680  scottexs  9847  scott0s  9848  aceq1  10077  dfac4  10082  dfac7  10093  dfac0  10094  dfac1  10095  dfac10  10098  dfac10c  10099  dfac10b  10100  kmlem4  10114  kmlem12  10122  kmlem14  10124  kmlem15  10125  kmlem16  10126  dfackm  10127  ac6n  10445  axpowndlem3  10559  zfcndrep  10574  zfcndun  10575  zfcndpow  10576  axgroth5  10784  axgroth2  10785  axgroth4  10792  grothprim  10794  sstskm  10802  fimaxre3  12136  infm3  12149  nnwos  12881  cotr2g  14949  brtrclfv  14975  trclfvcotr  14982  rpnnen2lem12  16200  isprm2  16659  vdwmc2  16957  pgpfac1  20019  pgpfac  20023  iunocv  21597  2ndcdisj2  23351  hausdiag  23539  rnelfmlem  23846  alexsubALTlem3  23943  cnextfun  23958  itg2leub  25642  eqscut2  27725  addsuniflem  27915  mulsuniflem  28059  onsfi  28254  mptelee  28829  nmoubi  30708  nmobndseqi  30715  nmobndseqiALT  30716  isch2  31159  isch3  31177  choc0  31262  nmopub  31844  nmfnleub  31861  xfree2  32381  mo5f  32425  nmo  32426  reuxfrdf  32427  rabsspr  32437  rabsstp  32438  inpr0  32468  cbvdisjf  32507  disjorf  32515  ssrelf  32550  funcnvmpt  32598  funcnv5mpt  32599  ssdifidlprm  33436  ballotlem2  34487  bnj89  34718  bnj115  34722  bnj1143  34787  bnj110  34855  bnj611  34915  bnj864  34919  bnj865  34920  bnj1000  34938  bnj978  34946  bnj1049  34971  bnj1052  34972  bnj1090  34976  bnj1030  34984  bnj1133  34986  bnj1171  34997  bnj1172  34998  bnj1174  35000  bnj1176  35002  bnj1204  35009  bnj1253  35014  bnj1388  35030  bnj1523  35068  fineqvrep  35092  fineqvpow  35093  vonf1owev  35102  axrepprim  35696  axunprim  35697  axpowprim  35698  axinfprim  35700  axacprim  35701  untuni  35703  dffr5  35748  elintfv  35759  dfon2lem8  35785  dfon2lem9  35786  19.12b  35796  brtxpsd3  35891  dfom5b  35907  dffun10  35909  disjeq1i  36187  ss-ax8  36220  cbvdisjvw2  36230  bj-notalbii  36609  bj-ssbeq  36648  bj-ax12ssb  36653  bj-hbext  36705  bj-nfalt  36706  bj-substax12  36716  bj-nnfalt  36761  bj-nnfext  36762  ax11-pm2  36831  bj-sblem  36839  eliminable-veqab  36861  eliminable-abeqv  36862  eliminable-abeqab  36863  bj-ralvw  36874  bj-sbeq  36896  bj-nfcf  36918  bj-snsetex  36958  bj-rcleqf  37020  bj-clex  37026  fvineqsneq  37407  wl-equsalvw  37533  wl-equsalcom  37538  wl-sb9v  37544  wl-sb8eft  37546  wl-sb8et  37548  wl-2sb6d  37553  wl-alanbii  37564  wl-sb8eut  37573  wl-sb8eutv  37574  poimirlem25  37646  poimirlem30  37651  heibor1lem  37810  sbcalfi  38117  mpobi123f  38163  mptbi12f  38167  ineccnvmo  38346  alrmomorn  38347  cocossss  38434  cossssid3  38467  cossssid4  38468  cosscnvssid4  38475  trcoss2  38482  dfeldisj4  38719  dfeldisj5  38720  disjres  38743  dvelimf-o  38929  axc11n-16  38938  pmapglbx  39770  sn-axrep5v  42211  abbibw  42672  dford4  43025  unielss  43214  onsupmaxb  43235  rp-fakeinunass  43511  rababg  43570  elmapintrab  43572  elinintrab  43573  undmrnresiss  43600  clss2lem  43607  cotrintab  43610  elintima  43649  relexp0eq  43697  dfhe3  43771  snhesn  43782  psshepw  43784  dffrege76  43935  frege77  43936  frege110  43969  dffrege115  43974  frege116  43975  frege118  43977  frege131  43990  ntrneikb  44090  ismnuprim  44290  rr-grothprimbi  44291  ismnushort  44297  rr-grothshortbi  44299  pm10.541  44363  pm10.542  44364  19.21vv  44372  19.31vv  44380  19.28vv  44382  pm11.62  44390  axc11next  44402  pm13.196a  44410  2sbc6g  44411  elnev  44434  hbexgVD  44902  dfac5prim  44987  permaxext  45002  permaxrep  45003  permaxpow  45006  permac8prim  45011  rabssf  45120  2rexsb  47106  dfich2  47463  ichal  47471  spr0nelg  47481  mo0sn  48808  dffun3f  49675  setrec1lem2  49681  setrec2  49688  setis  49691  alimp-surprise  49773  alimp-no-surprise  49774