Theorem albii 1852

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

This proof depends on syntax axioms:   ↔ wb 209  ∀wal 1568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210

This theorem is used by:  2albii  1853  3albii  1854  hbxfrbi  1858  alex  1859  2nalexn  1861  2exnaln  1862  imnang  1875  alexn  1878  19.26-2  1904  19.26-3an  1905  19.43OLD  1916  albiim  1922  2albiim  1923  empty  1939  19.32v  1973  19.31v  1974  19.23vv  1976  pm11.53v  1977  19.12vvv  2027  equsalvw  2037  2sb6  2123  sbrimvwOLD  2129  sbbiiev  2130  alrot3  2197  alrot4  2198  sbal  2206  sbalv  2207  19.21-2  2246  19.32  2270  19.31  2271  equsalv  2302  sbn  2314  sbrim  2338  aaan  2363  pm11.53  2376  19.12vv  2377  sb8v  2383  sb8f  2384  cbvsbvf  2393  equsal  2447  2sb6rf  2503  sbcom3  2536  sb8eulem  2624  eu1  2636  2mo2  2673  2eu1  2676  2eu1v  2677  2eu3  2679  euae  2685  nulmo  2738  eqabbw  2834  eqabcbw  2835  hblem  2892  hblemg  2893  eqabcb  2901  nfceqi  2920  eqabf  2952  ralbii2  3105  r2allem  3151  r3al  3201  r19.21t  3257  r19.23t  3259  ralcom4  3289  cbvralsvw  3314  sbralie  3339  sbralieOLD  3341  rabbi  3442  rabid2f  3443  rabid2im  3444  eqv  3461  eqvf  3462  abv  3463  abvALT  3464  ralv  3477  ceqsralt  3485  ceqsal  3488  ceqsalv  3490  rspc2gv  3586  ralxpxfr2d  3600  clel2g  3613  clel4g  3617  ralab  3651  ralrab2  3656  euind  3682  reu2  3683  reu3  3685  rmo4  3688  reu8  3691  rmo3f  3692  rmoim  3698  2reuswap  3704  2reuswap2  3705  reuind  3711  2reu5lem2  3714  2reu5lem3  3715  2rmoswap  3719  sbccomlem  3817  rmo2  3834  rmo3  3836  rmoanim  3842  dfss2  3917  ss2ab  4009  ss2rab  4017  rabss  4018  ss2rabd  4020  uniiunlem  4035  ssequn1  4132  unss  4136  ralunb  4143  ssin  4184  eq0f  4294  eq0  4297  eq0ALT  4298  ssdif0  4314  inssdif0OLD  4323  ab0w  4328  ab0  4329  ab0ALT  4330  ab0orv  4332  disj  4403  disj3  4407  ssundif  4443  ralf0  4453  ralidmw  4472  ralidm  4473  pwss  4581  rabsssn  4629  rabeqsnd  4630  ralsnsg  4631  ralsng  4636  disjsn  4672  snssb  4743  pwpw0  4774  dfnfc2  4889  unissb  4901  elintrab  4920  ssintrab  4931  intun  4940  intprg  4941  dfiin2g  4989  iunssf  5001  iunssfOLD  5002  iunss  5003  iunssOLD  5004  dfdisj2  5072  cbvdisj  5080  cbvdisjv  5081  disjor  5085  dftr2  5214  dftr5  5216  axrep1  5233  axrep4v  5237  axrep4  5238  axrep5  5239  axrep6  5240  zfrep6  5242  axsepgfromrep  5247  axnulALT  5258  vnexOLD  5272  inex1  5277  axpweq  5312  zfpow  5328  axpow2  5329  nfnid  5337  dtruALT  5350  reusv2lem4  5363  zfpair2  5392  prex  5396  el.OLD  5407  ssextss  5421  moabexOLD  5427  dffr6  5607  dffr2  5612  dffr2ALT  5613  dfepfr  5635  frinxp  5734  ssrel2  5761  eqrelrel  5773  raliunxp  5816  relop  5828  dmopab3  5901  dm0rn0  5906  dm0rn0OLD  5907  reldm0  5910  rnopab3  5938  iresn0n0  6046  dffr3  6097  cotrg  6105  idrefALT  6107  asymref  6110  asymref2  6111  intirr  6112  dffr4  6322  sucel  6438  sb8iota  6504  dffun6  6548  dffun3  6549  dffun4  6550  dffun5  6551  dffun6f  6552  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  7072  dff13  7256  fnssintima  7370  eqoprab2bw  7488  eqoprab2b  7489  mpo2eqb  7550  ralrnmpo  7557  imaeqalov  7658  zfun  7750  uniex2  7752  uniex2OLD  7753  funcnvuni  7942  ralxp3f  8147  frpoins3xpg  8150  frpoins3xp3g  8151  xpord3inddlem  8164  dfer2  8711  fiint  9311  marypha1lem  9418  marypha2lem3  9422  inf2  9617  axinf2  9634  ttrclss  9714  scottexsOLD  9936  scott0bsOLD  9938  setrec1lem2  9960  dffun3f  9968  setrec2  9970  aceq1  10189  dfac4  10194  dfac7  10204  dfac0  10205  dfac1  10206  dfac10  10209  dfac10c  10210  dfac10b  10211  kmlem4  10225  kmlem12  10233  kmlem14  10235  kmlem15  10236  kmlem16  10237  dfackm  10238  ac6n  10556  axpowndlem3  10677  zfcndrep  10692  zfcndun  10693  zfcndpow  10694  axgroth5  10902  axgroth2  10903  axgroth4  10910  grothprim  10912  sstskm  10920  fimaxre3  12256  infm3  12269  nnwos  13035  cotr2g  15122  brtrclfv  15148  trclfvcotr  15155  rpnnen2lem12  16386  isprm2  16850  vdwmc2  17150  pgpfac1  20289  pgpfac  20293  ssdifidlprm  21635  iunocv  21980  2ndcdisj2  23769  hausdiag  23957  rnelfmlem  24264  alexsubALTlem3  24361  cnextfun  24376  itg2leub  26048  eqcuts2  28165  addsuniflem  28380  mulsuniflem  28528  onsfi  28735  mpteleeOLD  29466  nmoubi  31367  nmobndseqi  31374  nmobndseqiALT  31375  isch2  31818  isch3  31836  choc0  31921  nmopub  32503  nmfnleub  32520  xfree2  33040  mo5f  33078  nmo  33079  reuxfrdf  33080  rabsspr  33090  rabsstp  33091  inpr0  33121  cbvdisjf  33158  disjorf  33166  ssrelf  33202  funcnv5mpt  33254  ballotlem2  35114  bnj89  35345  bnj115  35349  bnj1143  35413  bnj110  35481  bnj611  35541  bnj864  35545  bnj865  35546  bnj1000  35564  bnj978  35572  bnj1049  35597  bnj1052  35598  bnj1090  35602  bnj1030  35610  bnj1133  35612  bnj1171  35623  bnj1172  35624  bnj1174  35626  bnj1176  35628  bnj1204  35635  bnj1253  35640  bnj1388  35656  bnj1523  35694  axnulALT2  35704  fineqvrep  35765  fineqvpow  35766  axreg  35778  axregscl  35779  axregs  35790  axpowg  35797  vonf1wev  35870  vonf1owevOLD  35872  axrepprim  36446  axunprim  36447  axpowprim  36448  axinfprim  36450  axacprim  36451  untuni  36453  elintfv  36509  dfon2lem8  36532  dfon2lem9  36533  19.12b  36543  brtxpsd3  36638  dfom5b  36654  dffun10  36656  disjeq1i  36961  ss-ax8  36994  cbvdisjvw2  37004  mh-setind  37304  regsfromregtco  37306  regsfromsetind  37307  regsfromunir1  37308  mh-prprimbi  37311  mh-unprimbi  37312  mh-infprim1bi  37314  mh-infprim2bi  37315  mh-infprim3bi  37316  bj-notalbii  37479  bj-cbvaew  37523  bj-ssbeq  37532  bj-ax12ssb  37537  bj-nfalt  37595  bj-substax12  37606  bj-nnfalt  37672  bj-nnfext  37673  ax11-pm2  37728  bj-sblem  37736  eliminable-veqab  37758  eliminable-abeqv  37759  eliminable-abeqab  37760  bj-ralvw  37771  bj-sbeq  37793  bj-nfcf  37815  bj-snsetex  37856  bj-rcleqf  37918  bj-clex  37924  bj-rep  37969  bj-axseprep  37970  fvineqsneq  38315  wl-equsalvw  38450  wl-equsalcom  38455  wl-sb9v  38461  wl-sb8eft  38463  wl-sb8et  38465  wl-2sb6d  38470  wl-alanbii  38481  wl-sb8eut  38490  wl-sb8eutv  38491  poimirlem25  38543  poimirlem30  38548  heibor1lem  38723  sbcalfi  39028  mpobi123f  39074  mptbi12f  39078  ineccnvmo  39269  alrmomorn  39270  ralmo  39272  ralrmo3  39276  cocossss  39438  cossssid3  39471  cossssid4  39472  cosscnvssid4  39479  trcoss2  39486  dfeldisj4  39724  dfeldisj5  39725  disjres  39756  dvelimf-o  39966  axc11n-16  39975  pmapglbx  40806  sn-axrep5v  43251  abbibw  43668  dford4  44015  unielss  44204  onsupmaxb  44225  rp-fakeinunass  44500  rababg  44559  elmapintrab  44561  elinintrab  44562  undmrnresiss  44589  clss2lem  44596  cotrintab  44599  elintima  44638  relexp0eq  44686  dfhe3  44760  snhesn  44771  psshepw  44773  dffrege76  44924  frege77  44925  frege110  44958  dffrege115  44963  frege116  44964  frege118  44966  frege131  44979  ntrneikb  45079  ismnuprim  45263  rr-grothprimbi  45264  ismnushort  45270  rr-grothshortbi  45272  pm10.541  45336  pm10.542  45337  19.21vv  45345  19.31vv  45353  19.28vv  45355  pm11.62  45363  axc11next  45375  pm13.196a  45383  2sbc6g  45384  elnev  45406  hbexgVD  45873  dfac5prim  45958  permaxext  45973  permaxrep  45974  permaxpow  45977  permac8prim  45982  rabssf  46103  sinnpoly  47910  2rexsb  48140  dfich2  48509  ichal  48517  spr0nelg  48527  mo0sn  49895  setis  50760  alimp-surprise  50845  alimp-no-surprise  50846  dfrals2  50855  alsbii  50865  dfralseu2  50888  alseubii  50897  dfalseu2  50901