Theorem albii 1849

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

Syntax hints:   ↔ wb 209  ∀wal 1568

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

This theorem depends on definitions:  df-bi 210

This theorem is referenced by:  2albii  1850  3albii  1851  hbxfrbi  1855  alex  1856  2nalexn  1858  2exnaln  1859  imnang  1872  alexn  1875  19.26-2  1901  19.26-3an  1902  19.43OLD  1913  albiim  1919  2albiim  1920  empty  1936  19.32v  1970  19.31v  1971  19.23vv  1973  pm11.53v  1974  19.12vvv  2024  equsalvw  2034  2sb6  2120  sbrimvwOLD  2126  sbbiiev  2127  alrot3  2195  alrot4  2196  sbal  2204  sbalv  2205  19.21-2  2245  19.32  2269  19.31  2270  equsalv  2303  sbn  2315  sbrim  2339  aaan  2365  pm11.53  2378  19.12vv  2379  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  eqabbw  2836  eqabcbw  2837  hblem  2894  hblemg  2895  eqabcb  2903  nfceqi  2922  eqabf  2954  ralbii2  3107  r2allem  3153  r3al  3203  r19.21t  3259  r19.23t  3261  ralcom4  3291  cbvralsvw  3316  sbralie  3342  sbralieOLD  3344  rabbi  3446  rabid2f  3447  rabid2im  3448  eqv  3465  eqvf  3466  abv  3467  abvALT  3468  ralv  3481  ceqsralt  3489  ceqsal  3492  ceqsalv  3494  rspc2gv  3592  ralxpxfr2d  3606  clel2g  3619  clel4g  3623  ralab  3657  ralrab2  3662  euind  3688  reu2  3689  reu3  3691  rmo4  3694  reu8  3697  rmo3f  3698  rmoim  3704  2reuswap  3710  2reuswap2  3711  reuind  3717  2reu5lem2  3720  2reu5lem3  3721  2rmoswap  3725  sbccomlem  3823  rmo2  3841  rmo3  3843  rmoanim  3849  dfss2  3924  ss2ab  4016  ss2rab  4024  rabss  4025  ss2rabd  4027  uniiunlem  4042  dfdif3OLD  4074  ssequn1  4140  unss  4144  ralunb  4151  ssin  4192  eq0f  4302  eq0  4305  eq0ALT  4306  ssdif0  4322  inssdif0OLD  4331  ab0w  4336  ab0  4337  ab0ALT  4338  ab0orv  4340  disj  4411  disj3  4415  ssundif  4449  ralf0  4459  ralidmw  4478  ralidm  4479  pwss  4587  rabsssn  4635  rabeqsnd  4636  ralsnsg  4637  ralsng  4642  disjsn  4678  snssb  4749  pwpw0  4780  dfnfc2  4895  unissb  4907  elintrab  4926  ssintrab  4937  intun  4946  intprg  4947  dfiin2g  4996  iunssf  5008  iunssfOLD  5009  iunss  5010  iunssOLD  5011  dfdisj2  5079  cbvdisj  5087  cbvdisjv  5088  disjor  5092  dftr2  5221  dftr5  5223  axrep1  5240  axrep4v  5244  axrep4  5245  axrep5  5247  axrep6  5248  axrep6OLD  5249  zfrep6  5251  axsepgfromrep  5256  axnulALT  5268  vnexOLD  5282  inex1  5287  axpweq  5323  zfpow  5339  axpow2  5340  nfnid  5348  dtruALT  5361  reusv2lem4  5374  zfpair2  5407  prex  5411  elOLD  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  6323  sucel  6439  sb8iota  6505  dffun6  6549  dffun3  6550  dffun4  6551  dffun5  6552  dffun6f  6553  dffun7  6565  funopab  6573  funcnv2  6606  funcnv  6607  fun2cnv  6609  fun11  6612  fununi  6613  fnres  6664  mptfnf  6672  fnopabg  6674  tz6.12-2  6870  brprcneu  6873  brprcneuALT  6874  dffv2  6978  funcnvmpt  6993  fvn0ssdmfun  7071  dff13  7254  fnssintima  7362  eqoprab2bw  7482  eqoprab2b  7483  mpo2eqb  7544  ralrnmpo  7551  imaeqalov  7651  zfun  7735  uniex2  7737  uniex2OLD  7738  funcnvuni  7930  ralxp3f  8134  frpoins3xpg  8137  frpoins3xp3g  8138  xpord3inddlem  8151  dfer2  8696  fiint  9287  marypha1lem  9394  marypha2lem3  9398  inf2  9593  axinf2  9610  ttrclss  9690  scottexs  9862  scott0s  9863  aceq1  10102  dfac4  10107  dfac7  10117  dfac0  10118  dfac1  10119  dfac10  10122  dfac10c  10123  dfac10b  10124  kmlem4  10138  kmlem12  10146  kmlem14  10148  kmlem15  10149  kmlem16  10150  dfackm  10151  ac6n  10470  axpowndlem3  10585  zfcndrep  10600  zfcndun  10601  zfcndpow  10602  axgroth5  10810  axgroth2  10811  axgroth4  10818  grothprim  10820  sstskm  10828  fimaxre3  12162  infm3  12175  nnwos  12940  cotr2g  15015  brtrclfv  15041  trclfvcotr  15048  rpnnen2lem12  16282  isprm2  16741  vdwmc2  17040  pgpfac1  20153  pgpfac  20157  ssdifidlprm  21467  iunocv  21812  2ndcdisj2  23595  hausdiag  23783  rnelfmlem  24090  alexsubALTlem3  24187  cnextfun  24202  itg2leub  25874  eqcuts2  27960  addsuniflem  28175  mulsuniflem  28323  onsfi  28530  mpteleeOLD  29226  nmoubi  31105  nmobndseqi  31112  nmobndseqiALT  31113  isch2  31556  isch3  31574  choc0  31659  nmopub  32241  nmfnleub  32258  xfree2  32778  mo5f  32816  nmo  32817  reuxfrdf  32818  rabsspr  32828  rabsstp  32829  inpr0  32859  cbvdisjf  32897  disjorf  32905  ssrelf  32941  funcnv5mpt  32993  ballotlem2  34860  bnj89  35091  bnj115  35095  bnj1143  35159  bnj110  35227  bnj611  35287  bnj864  35291  bnj865  35292  bnj1000  35310  bnj978  35318  bnj1049  35343  bnj1052  35344  bnj1090  35348  bnj1030  35356  bnj1133  35358  bnj1171  35369  bnj1172  35370  bnj1174  35372  bnj1176  35374  bnj1204  35381  bnj1253  35386  bnj1388  35402  bnj1523  35440  axnulALT2  35452  fineqvrep  35508  fineqvpow  35509  axreg  35521  axregscl  35522  axregs  35533  axpowg  35540  vonf1wev  35573  vonf1owevOLD  35575  axrepprim  36175  axunprim  36176  axpowprim  36177  axinfprim  36179  axacprim  36180  untuni  36182  dffr5  36227  elintfv  36238  dfon2lem8  36261  dfon2lem9  36262  19.12b  36272  brtxpsd3  36367  dfom5b  36383  dffun10  36385  disjeq1i  36685  ss-ax8  36718  cbvdisjvw2  36728  mh-setind  37028  regsfromregtco  37030  regsfromsetind  37031  regsfromunir1  37032  mh-prprimbi  37035  mh-unprimbi  37036  mh-infprim1bi  37038  mh-infprim2bi  37039  mh-infprim3bi  37040  bj-notalbii  37203  bj-cbvaew  37247  bj-ssbeq  37256  bj-ax12ssb  37261  bj-nfalt  37319  bj-substax12  37330  bj-nnfalt  37396  bj-nnfext  37397  ax11-pm2  37452  bj-sblem  37460  eliminable-veqab  37482  eliminable-abeqv  37483  eliminable-abeqab  37484  bj-ralvw  37495  bj-sbeq  37517  bj-nfcf  37539  bj-snsetex  37580  bj-rcleqf  37642  bj-clex  37648  bj-rep  37691  bj-axseprep  37692  fvineqsneq  38039  wl-equsalvw  38174  wl-equsalcom  38179  wl-sb9v  38185  wl-sb8eft  38187  wl-sb8et  38189  wl-2sb6d  38194  wl-alanbii  38205  wl-sb8eut  38214  wl-sb8eutv  38215  poimirlem25  38277  poimirlem30  38282  heibor1lem  38441  sbcalfi  38746  mpobi123f  38792  mptbi12f  38796  ineccnvmo  38987  alrmomorn  38988  ralmo  38990  ralrmo3  38994  cocossss  39156  cossssid3  39189  cossssid4  39190  cosscnvssid4  39197  trcoss2  39204  dfeldisj4  39442  dfeldisj5  39443  disjres  39474  dvelimf-o  39684  axc11n-16  39693  pmapglbx  40524  sn-axrep5v  42969  abbibw  43392  dford4  43739  unielss  43928  onsupmaxb  43949  rp-fakeinunass  44224  rababg  44283  elmapintrab  44285  elinintrab  44286  undmrnresiss  44313  clss2lem  44320  cotrintab  44323  elintima  44362  relexp0eq  44410  dfhe3  44484  snhesn  44495  psshepw  44497  dffrege76  44648  frege77  44649  frege110  44682  dffrege115  44687  frege116  44688  frege118  44690  frege131  44703  ntrneikb  44803  ismnuprim  44987  rr-grothprimbi  44988  ismnushort  44994  rr-grothshortbi  44996  pm10.541  45060  pm10.542  45061  19.21vv  45069  19.31vv  45077  19.28vv  45079  pm11.62  45087  axc11next  45099  pm13.196a  45107  2sbc6g  45108  elnev  45130  hbexgVD  45597  dfac5prim  45682  permaxext  45697  permaxrep  45698  permaxpow  45701  permac8prim  45706  rabssf  45820  sinnpoly  47611  2rexsb  47821  dfich2  48190  ichal  48198  spr0nelg  48208  mo0sn  49577  dffun3f  50443  setrec1lem2  50449  setrec2  50456  setis  50459  alimp-surprise  50541  alimp-no-surprise  50542  dfrals2  50551  alsbii  50561