Theorem albii 1817

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

Syntax hints:   ↔ wb 206  ∀wal 1535

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

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  2albii  1818  3albii  1819  hbxfrbi  1823  alex  1824  2nalexn  1826  2exnaln  1827  imnang  1840  alexn  1843  nfnbiOLD  1854  19.26-2  1870  19.26-3an  1871  19.43OLD  1882  albiim  1888  2albiim  1889  empty  1905  19.32v  1939  19.31v  1940  19.23vv  1942  pm11.53v  1943  19.12vvv  1988  equsalvw  2003  2sb6  2086  sbrimvw  2091  sbbiiev  2092  alrot3  2161  alrot4  2162  sbal  2170  sbalv  2171  19.21-2  2210  19.32  2234  19.31  2235  equsalv  2268  sbn  2284  sbrim  2308  sbnfOLD  2317  aaan  2337  aaanOLD  2338  pm11.53  2352  19.12vv  2353  sb8v  2358  sb8f  2359  cbvsbvf  2369  equsal  2425  2sb6rf  2481  sbcom3  2514  sb8eulem  2601  eu1  2613  2mo2  2650  2eu1  2654  2eu1v  2655  2eu3  2657  euae  2663  nulmo  2716  eqabbw  2818  hblem  2876  hblemg  2877  eqabbOLD  2885  eqabcb  2886  nfceqi  2905  eqabf  2941  ralbii2  3095  r2allem  3148  r19.21vOLD  3187  r3al  3203  r19.21t  3259  r19.23t  3261  ralcom4  3292  ralcom4OLD  3293  nfra2wOLD  3306  cbvralsvw  3323  sbralie  3366  moelOLD  3413  rabbi  3475  rabid2f  3476  rabid2im  3477  rabid2OLD  3479  eqv  3498  eqvf  3499  abv  3500  abvALT  3501  ralv  3516  ceqsralt  3524  ceqsal  3527  ceqsalv  3529  rspc2gv  3645  ralxpxfr2d  3659  clel2g  3672  clel4g  3676  elabgtOLD  3686  elabg  3690  ralab  3713  ralabOLD  3714  ralrab2  3720  euind  3746  reu2  3747  reu3  3749  rmo4  3752  reu8  3755  rmo3f  3756  rmoim  3762  2reuswap  3768  2reuswap2  3769  reuind  3775  2reu5lem2  3778  2reu5lem3  3779  2rmoswap  3783  sbccomlem  3891  rmo2  3909  rmo3  3911  rmoanim  3916  dfss2  3994  ss2ab  4085  ss2rab  4094  rabss  4095  uniiunlem  4110  dfdif3OLD  4141  ssequn1  4209  unss  4213  ralunb  4220  ssin  4260  vn0  4368  eq0f  4370  eq0  4373  eq0ALT  4374  ssdif0  4389  inssdif0  4397  ab0w  4401  ab0  4402  ab0OLD  4403  ab0ALT  4404  ab0orv  4406  eq0rdv  4430  disj  4473  disj3  4477  ssundif  4511  ralidmw  4531  ralidm  4535  ralf0  4537  pwss  4645  rabsssn  4690  rabeqsnd  4691  ralsnsg  4692  ralsng  4697  disjsn  4736  snssb  4807  snssgOLD  4809  pwpw0  4838  dfnfc2  4953  unissb  4963  unissbOLD  4964  elintrab  4984  ssintrab  4995  intun  5004  intprg  5005  dfiin2g  5055  iunssf  5067  iunss  5068  dfdisj2  5135  cbvdisj  5143  cbvdisjv  5144  disjor  5148  dftr2  5285  dftr5  5287  dftr5OLD  5288  axrep1  5304  axrep5  5309  axrep6  5310  axsepgfromrep  5315  axnulALT  5322  vnex  5332  inex1  5335  axpweq  5369  zfpow  5384  axpow2  5385  axpow3  5386  nfnid  5393  dtruALT  5406  reusv2lem4  5419  zfpair2  5448  el  5457  ssextss  5473  moabex  5479  dffr6  5655  dffr2  5661  dffr2ALT  5662  dfepfr  5684  frinxp  5782  ssrel2  5809  eqrelrel  5821  reliun  5840  raliunxp  5864  relop  5875  dmopab3  5944  dm0rn0  5949  reldm0  5952  iresn0n0  6083  dffr3  6129  cotrg  6139  cotrgOLD  6140  cotrgOLDOLD  6141  idrefALT  6143  asymref  6148  asymref2  6149  intirr  6150  dffr4  6352  sucel  6469  sb8iota  6537  dffun2OLDOLD  6585  dffun6  6586  dffun3  6587  dffun3OLD  6588  dffun4  6589  dffun5  6590  dffun6f  6591  dffun7  6605  funopab  6613  funcnv2  6646  funcnv  6647  fun2cnv  6649  fun11  6652  fununi  6653  fnres  6707  mptfnf  6715  fnopabg  6717  brprcneu  6910  brprcneuALT  6911  dffv2  7017  fvn0ssdmfun  7108  dff13  7292  fnssintima  7398  eqoprab2bw  7520  eqoprab2b  7521  mpo2eqb  7582  ralrnmpo  7589  imaeqalov  7689  zfun  7771  uniex2  7773  funcnvuni  7972  ralxp3f  8178  frpoins3xpg  8181  frpoins3xp3g  8182  xpord3inddlem  8195  dfer2  8764  fiint  9394  fiintOLD  9395  marypha1lem  9502  marypha2lem3  9506  inf2  9692  axinf2  9709  ttrclss  9789  scottexs  9956  scott0s  9957  aceq1  10186  dfac4  10191  dfac7  10202  dfac0  10203  dfac1  10204  dfac10  10207  dfac10c  10208  dfac10b  10209  kmlem4  10223  kmlem12  10231  kmlem14  10233  kmlem15  10234  kmlem16  10235  dfackm  10236  ac6n  10554  axpowndlem3  10668  zfcndrep  10683  zfcndun  10684  zfcndpow  10685  axgroth5  10893  axgroth2  10894  axgroth4  10901  grothprim  10903  sstskm  10911  fimaxre3  12241  infm3  12254  nnwos  12980  cotr2g  15025  brtrclfv  15051  trclfvcotr  15058  rpnnen2lem12  16273  isprm2  16729  vdwmc2  17026  pgpfac1  20124  pgpfac  20128  iunocv  21722  2ndcdisj2  23486  hausdiag  23674  rnelfmlem  23981  alexsubALTlem3  24078  cnextfun  24093  itg2leub  25789  eqscut2  27869  addsuniflem  28052  mulsuniflem  28193  mptelee  28928  nmoubi  30804  nmobndseqi  30811  nmobndseqiALT  30812  isch2  31255  isch3  31273  choc0  31358  nmopub  31940  nmfnleub  31957  xfree2  32477  mo5f  32517  nmo  32518  reuxfrdf  32519  rabsspr  32529  rabsstp  32530  inpr0  32560  cbvdisjf  32593  disjorf  32601  ssrelf  32637  funcnvmpt  32685  funcnv5mpt  32686  ssdifidlprm  33451  ballotlem2  34453  bnj89  34697  bnj115  34701  bnj1143  34766  bnj110  34834  bnj611  34894  bnj864  34898  bnj865  34899  bnj1000  34917  bnj978  34925  bnj1049  34950  bnj1052  34951  bnj1090  34955  bnj1030  34963  bnj1133  34965  bnj1171  34976  bnj1172  34977  bnj1174  34979  bnj1176  34981  bnj1204  34988  bnj1253  34993  bnj1388  35009  bnj1523  35047  fineqvrep  35071  fineqvpow  35072  axrepprim  35664  axunprim  35665  axpowprim  35666  axinfprim  35668  axacprim  35669  untuni  35671  dffr5  35716  elintfv  35728  dfon2lem8  35754  dfon2lem9  35755  19.12b  35765  brtxpsd3  35860  dfom5b  35876  dffun10  35878  disjeq1i  36156  ss-ax8  36191  cbvdisjvw2  36201  bj-notalbii  36580  bj-ssbeq  36619  bj-ax12ssb  36624  bj-hbext  36676  bj-nfalt  36677  bj-substax12  36687  bj-nnfalt  36732  bj-nnfext  36733  ax11-pm2  36802  bj-sblem  36810  eliminable-veqab  36832  eliminable-abeqv  36833  eliminable-abeqab  36834  bj-ralvw  36845  bj-sbeq  36867  bj-nfcf  36889  bj-snsetex  36929  bj-rcleqf  36991  bj-clex  36997  fvineqsneq  37378  wl-equsalvw  37492  wl-equsalcom  37497  wl-sb9v  37503  wl-sb8eft  37505  wl-sb8et  37507  wl-2sb6d  37512  wl-alanbii  37523  wl-sb8eut  37532  wl-sb8eutv  37533  poimirlem25  37605  poimirlem30  37610  heibor1lem  37769  sbcalfi  38076  mpobi123f  38122  mptbi12f  38126  ineccnvmo  38313  alrmomorn  38314  cocossss  38392  cossssid3  38425  cossssid4  38426  cosscnvssid4  38433  trcoss2  38440  dfeldisj4  38676  dfeldisj5  38677  disjres  38700  dvelimf-o  38885  axc11n-16  38894  pmapglbx  39726  sn-axrep5v  42209  abbibw  42632  dford4  42986  unielss  43179  onsupmaxb  43200  rp-fakeinunass  43477  rababg  43536  elmapintrab  43538  elinintrab  43539  undmrnresiss  43566  clss2lem  43573  cotrintab  43576  elintima  43615  relexp0eq  43663  dfhe3  43737  snhesn  43748  psshepw  43750  dffrege76  43901  frege77  43902  frege110  43935  dffrege115  43940  frege116  43941  frege118  43943  frege131  43956  ntrneikb  44056  ismnuprim  44263  rr-grothprimbi  44264  ismnushort  44270  rr-grothshortbi  44272  pm10.541  44336  pm10.542  44337  19.21vv  44345  19.31vv  44353  19.28vv  44355  pm11.62  44363  axc11next  44375  pm13.196a  44383  2sbc6g  44384  elnev  44407  hbexgVD  44877  rabssf  45021  2rexsb  47016  dfich2  47332  ichal  47340  spr0nelg  47350  mo0sn  48547  dffun3f  48774  setrec1lem2  48780  setrec2  48787  setis  48790  alimp-surprise  48874  alimp-no-surprise  48875