Theorem albii 1820

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

Syntax hints:   ↔ wb 206  ∀wal 1539

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

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  2albii  1821  3albii  1822  hbxfrbi  1826  alex  1827  2nalexn  1829  2exnaln  1830  imnang  1843  alexn  1846  19.26-2  1872  19.26-3an  1873  19.43OLD  1884  albiim  1890  2albiim  1891  empty  1907  19.32v  1941  19.31v  1942  19.23vv  1944  pm11.53v  1945  19.12vvv  1995  equsalvw  2005  2sb6  2089  sbrimvw  2094  sbbiiev  2095  alrot3  2163  alrot4  2164  sbal  2172  sbalv  2173  19.21-2  2212  19.32  2236  19.31  2237  equsalv  2270  sbn  2282  sbrim  2306  sbnfOLD  2314  aaan  2333  pm11.53  2346  19.12vv  2347  sb8v  2353  sb8f  2354  cbvsbvf  2363  equsal  2417  2sb6rf  2473  sbcom3  2506  sb8eulem  2593  eu1  2605  2mo2  2642  2eu1  2646  2eu1v  2647  2eu3  2649  euae  2655  nulmo  2708  eqabbw  2804  eqabcbw  2805  hblem  2862  hblemg  2863  eqabbOLD  2871  eqabcb  2872  nfceqi  2891  eqabf  2924  ralbii2  3074  r2allem  3120  r3al  3170  r19.21t  3226  r19.23t  3228  ralcom4  3258  cbvralsvw  3283  sbralie  3318  sbralieOLD  3320  rabbi  3425  rabid2f  3426  rabid2im  3427  eqv  3446  eqvf  3447  abv  3448  abvALT  3449  ralv  3463  ceqsralt  3471  ceqsal  3474  ceqsalv  3476  rspc2gv  3587  ralxpxfr2d  3601  clel2g  3614  clel4g  3618  elabgtOLDOLD  3629  ralab  3652  ralrab2  3657  euind  3683  reu2  3684  reu3  3686  rmo4  3689  reu8  3692  rmo3f  3693  rmoim  3699  2reuswap  3705  2reuswap2  3706  reuind  3712  2reu5lem2  3715  2reu5lem3  3716  2rmoswap  3720  sbccomlem  3820  rmo2  3838  rmo3  3840  rmoanim  3845  dfss2  3920  ss2ab  4013  ss2rab  4021  rabss  4022  uniiunlem  4037  dfdif3OLD  4068  ssequn1  4136  unss  4140  ralunb  4147  ssin  4189  vn0  4295  eq0f  4297  eq0  4300  eq0ALT  4301  ssdif0  4316  inssdif0  4324  ab0w  4329  ab0  4330  ab0ALT  4331  ab0orv  4333  eq0rdv  4357  disj  4400  disj3  4404  ssundif  4438  ralidmw  4458  ralidm  4462  ralf0  4464  pwss  4573  rabsssn  4621  rabeqsnd  4622  ralsnsg  4623  ralsng  4628  disjsn  4664  snssb  4735  pwpw0  4765  dfnfc2  4881  unissb  4891  elintrab  4910  ssintrab  4921  intun  4930  intprg  4931  dfiin2g  4981  iunssf  4993  iunss  4994  dfdisj2  5060  cbvdisj  5068  cbvdisjv  5069  disjor  5073  dftr2  5200  dftr5  5202  axrep1  5218  axrep4v  5222  axrep4  5223  axrep5  5225  axrep6  5226  axrep6OLD  5227  axsepgfromrep  5232  axnulALT  5242  vnex  5252  inex1  5255  axpweq  5289  zfpow  5304  axpow2  5305  nfnid  5313  dtruALT  5326  reusv2lem4  5339  zfpair2  5371  el  5380  ssextss  5394  moabex  5399  dffr6  5572  dffr2  5577  dffr2ALT  5578  dfepfr  5600  frinxp  5699  ssrel2  5725  eqrelrel  5737  reliun  5756  raliunxp  5779  relop  5790  dmopab3  5859  dm0rn0  5864  dm0rn0OLD  5865  reldm0  5868  rnopab3  5896  iresn0n0  6003  dffr3  6048  cotrg  6058  idrefALT  6060  asymref  6063  asymref2  6064  intirr  6065  dffr4  6267  sucel  6382  sb8iota  6448  dffun6  6492  dffun3  6493  dffun4  6494  dffun5  6495  dffun6f  6496  dffun7  6508  funopab  6516  funcnv2  6549  funcnv  6550  fun2cnv  6552  fun11  6555  fununi  6556  fnres  6608  mptfnf  6616  fnopabg  6618  tz6.12-2  6809  brprcneu  6812  brprcneuALT  6813  dffv2  6917  fvn0ssdmfun  7007  dff13  7188  fnssintima  7296  eqoprab2bw  7416  eqoprab2b  7417  mpo2eqb  7478  ralrnmpo  7485  imaeqalov  7585  zfun  7669  uniex2  7671  funcnvuni  7862  ralxp3f  8067  frpoins3xpg  8070  frpoins3xp3g  8071  xpord3inddlem  8084  dfer2  8623  fiint  9211  marypha1lem  9317  marypha2lem3  9321  inf2  9513  axinf2  9530  ttrclss  9610  scottexs  9780  scott0s  9781  aceq1  10008  dfac4  10013  dfac7  10024  dfac0  10025  dfac1  10026  dfac10  10029  dfac10c  10030  dfac10b  10031  kmlem4  10045  kmlem12  10053  kmlem14  10055  kmlem15  10056  kmlem16  10057  dfackm  10058  ac6n  10376  axpowndlem3  10490  zfcndrep  10505  zfcndun  10506  zfcndpow  10507  axgroth5  10715  axgroth2  10716  axgroth4  10723  grothprim  10725  sstskm  10733  fimaxre3  12068  infm3  12081  nnwos  12813  cotr2g  14883  brtrclfv  14909  trclfvcotr  14916  rpnnen2lem12  16134  isprm2  16593  vdwmc2  16891  pgpfac1  19995  pgpfac  19999  iunocv  21619  2ndcdisj2  23373  hausdiag  23561  rnelfmlem  23868  alexsubALTlem3  23965  cnextfun  23980  itg2leub  25663  eqscut2  27748  addsuniflem  27945  mulsuniflem  28089  onsfi  28284  mptelee  28874  nmoubi  30750  nmobndseqi  30757  nmobndseqiALT  30758  isch2  31201  isch3  31219  choc0  31304  nmopub  31886  nmfnleub  31903  xfree2  32423  mo5f  32466  nmo  32467  reuxfrdf  32468  rabsspr  32479  rabsstp  32480  inpr0  32510  cbvdisjf  32549  disjorf  32557  ssrelf  32596  funcnvmpt  32647  funcnv5mpt  32648  ssdifidlprm  33421  ballotlem2  34500  bnj89  34731  bnj115  34735  bnj1143  34800  bnj110  34868  bnj611  34928  bnj864  34932  bnj865  34933  bnj1000  34951  bnj978  34959  bnj1049  34984  bnj1052  34985  bnj1090  34989  bnj1030  34997  bnj1133  34999  bnj1171  35010  bnj1172  35011  bnj1174  35013  bnj1176  35015  bnj1204  35022  bnj1253  35027  bnj1388  35043  bnj1523  35081  axreg  35123  axregscl  35124  fineqvrep  35135  fineqvpow  35136  axregs  35143  vonf1owev  35150  axrepprim  35744  axunprim  35745  axpowprim  35746  axinfprim  35748  axacprim  35749  untuni  35751  dffr5  35796  elintfv  35807  dfon2lem8  35830  dfon2lem9  35831  19.12b  35841  brtxpsd3  35936  dfom5b  35952  dffun10  35954  disjeq1i  36232  ss-ax8  36265  cbvdisjvw2  36275  bj-notalbii  36654  bj-ssbeq  36693  bj-ax12ssb  36698  bj-hbext  36750  bj-nfalt  36751  bj-substax12  36761  bj-nnfalt  36806  bj-nnfext  36807  ax11-pm2  36876  bj-sblem  36884  eliminable-veqab  36906  eliminable-abeqv  36907  eliminable-abeqab  36908  bj-ralvw  36919  bj-sbeq  36941  bj-nfcf  36963  bj-snsetex  37003  bj-rcleqf  37065  bj-clex  37071  fvineqsneq  37452  wl-equsalvw  37578  wl-equsalcom  37583  wl-sb9v  37589  wl-sb8eft  37591  wl-sb8et  37593  wl-2sb6d  37598  wl-alanbii  37609  wl-sb8eut  37618  wl-sb8eutv  37619  poimirlem25  37691  poimirlem30  37696  heibor1lem  37855  sbcalfi  38162  mpobi123f  38208  mptbi12f  38212  ineccnvmo  38391  alrmomorn  38392  cocossss  38479  cossssid3  38512  cossssid4  38513  cosscnvssid4  38520  trcoss2  38527  dfeldisj4  38764  dfeldisj5  38765  disjres  38788  dvelimf-o  38974  axc11n-16  38983  pmapglbx  39814  sn-axrep5v  42255  abbibw  42716  dford4  43068  unielss  43257  onsupmaxb  43278  rp-fakeinunass  43554  rababg  43613  elmapintrab  43615  elinintrab  43616  undmrnresiss  43643  clss2lem  43650  cotrintab  43653  elintima  43692  relexp0eq  43740  dfhe3  43814  snhesn  43825  psshepw  43827  dffrege76  43978  frege77  43979  frege110  44012  dffrege115  44017  frege116  44018  frege118  44020  frege131  44033  ntrneikb  44133  ismnuprim  44333  rr-grothprimbi  44334  ismnushort  44340  rr-grothshortbi  44342  pm10.541  44406  pm10.542  44407  19.21vv  44415  19.31vv  44423  19.28vv  44425  pm11.62  44433  axc11next  44445  pm13.196a  44453  2sbc6g  44454  elnev  44476  hbexgVD  44944  dfac5prim  45029  permaxext  45044  permaxrep  45045  permaxpow  45048  permac8prim  45053  rabssf  45162  sinnpoly  46928  2rexsb  47138  dfich2  47495  ichal  47503  spr0nelg  47513  mo0sn  48853  dffun3f  49720  setrec1lem2  49726  setrec2  49733  setis  49736  alimp-surprise  49818  alimp-no-surprise  49819