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  2245  19.32  2269  19.31  2270  equsalv  2301  sbn  2313  sbrim  2337  aaan  2362  pm11.53  2375  19.12vv  2376  sb8v  2382  sb8f  2383  cbvsbvf  2392  equsal  2446  2sb6rf  2502  sbcom3  2535  sb8eulem  2623  eu1  2635  2mo2  2672  2eu1  2675  2eu1v  2676  2eu3  2678  euae  2684  nulmo  2737  eqabbw  2833  eqabcbw  2834  hblem  2891  hblemg  2892  eqabcb  2900  nfceqi  2919  eqabf  2951  ralbii2  3104  r2allem  3150  r3al  3200  r19.21t  3256  r19.23t  3258  ralcom4  3288  cbvralsvw  3313  sbralie  3338  sbralieOLD  3340  rabbi  3441  rabid2f  3442  rabid2im  3443  eqv  3460  eqvf  3461  abv  3462  abvALT  3463  ralv  3476  ceqsralt  3484  ceqsal  3487  ceqsalv  3489  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  5240  axrep6  5241  axrep6OLD  5242  zfrep6  5244  axsepgfromrep  5249  axnulALT  5261  vnexOLD  5275  inex1  5280  axpweq  5315  zfpow  5331  axpow2  5332  nfnid  5340  dtruALT  5353  reusv2lem4  5366  zfpair2  5399  prex  5403  el.OLD  5414  ssextss  5428  moabexOLD  5434  dffr6  5611  dffr2  5616  dffr2ALT  5617  dfepfr  5639  frinxp  5738  ssrel2  5765  eqrelrel  5777  raliunxp  5819  relop  5830  dmopab3  5903  dm0rn0  5908  dm0rn0OLD  5909  reldm0  5912  rnopab3  5940  iresn0n0  6050  dffr3  6095  cotrg  6105  idrefALT  6107  asymref  6110  asymref2  6111  intirr  6112  dffr4  6318  sucel  6434  sb8iota  6500  dffun6  6544  dffun3  6545  dffun4  6546  dffun5  6547  dffun6f  6548  dffun7  6560  funopab  6568  funcnv2  6601  funcnv  6602  fun2cnv  6604  fun11  6607  fununi  6608  fnres  6659  mptfnf  6667  fnopabg  6669  tz6.12-2  6865  brprcneu  6868  brprcneuALT  6869  dffv2  6973  funcnvmpt  6988  fvn0ssdmfun  7067  dff13  7251  fnssintima  7365  eqoprab2bw  7483  eqoprab2b  7484  mpo2eqb  7545  ralrnmpo  7552  imaeqalov  7653  zfun  7737  uniex2  7739  uniex2OLD  7740  funcnvuni  7929  ralxp3f  8135  frpoins3xpg  8138  frpoins3xp3g  8139  xpord3inddlem  8152  dfer2  8697  fiint  9296  marypha1lem  9403  marypha2lem3  9407  inf2  9602  axinf2  9619  ttrclss  9699  scottexsOLD  9882  scott0bsOLD  9884  aceq1  10120  dfac4  10125  dfac7  10135  dfac0  10136  dfac1  10137  dfac10  10140  dfac10c  10141  dfac10b  10142  kmlem4  10156  kmlem12  10164  kmlem14  10166  kmlem15  10167  kmlem16  10168  dfackm  10169  ac6n  10487  axpowndlem3  10608  zfcndrep  10623  zfcndun  10624  zfcndpow  10625  axgroth5  10833  axgroth2  10834  axgroth4  10841  grothprim  10843  sstskm  10851  fimaxre3  12185  infm3  12198  nnwos  12964  cotr2g  15049  brtrclfv  15075  trclfvcotr  15082  rpnnen2lem12  16313  isprm2  16772  vdwmc2  17071  pgpfac1  20209  pgpfac  20213  ssdifidlprm  21549  iunocv  21894  2ndcdisj2  23683  hausdiag  23871  rnelfmlem  24178  alexsubALTlem3  24275  cnextfun  24290  itg2leub  25962  eqcuts2  28051  addsuniflem  28266  mulsuniflem  28414  onsfi  28621  mpteleeOLD  29352  nmoubi  31253  nmobndseqi  31260  nmobndseqiALT  31261  isch2  31704  isch3  31722  choc0  31807  nmopub  32389  nmfnleub  32406  xfree2  32926  mo5f  32964  nmo  32965  reuxfrdf  32966  rabsspr  32976  rabsstp  32977  inpr0  33007  cbvdisjf  33044  disjorf  33052  ssrelf  33088  funcnv5mpt  33140  ballotlem2  35000  bnj89  35231  bnj115  35235  bnj1143  35299  bnj110  35367  bnj611  35427  bnj864  35431  bnj865  35432  bnj1000  35450  bnj978  35458  bnj1049  35483  bnj1052  35484  bnj1090  35488  bnj1030  35496  bnj1133  35498  bnj1171  35509  bnj1172  35510  bnj1174  35512  bnj1176  35514  bnj1204  35521  bnj1253  35526  bnj1388  35542  bnj1523  35580  axnulALT2  35590  fineqvrep  35640  fineqvpow  35641  axreg  35653  axregscl  35654  axregs  35665  axpowg  35672  vonf1wev  35705  vonf1owevOLD  35707  axrepprim  36281  axunprim  36282  axpowprim  36283  axinfprim  36285  axacprim  36286  untuni  36288  elintfv  36344  dfon2lem8  36367  dfon2lem9  36368  19.12b  36378  brtxpsd3  36473  dfom5b  36489  dffun10  36491  disjeq1i  36812  ss-ax8  36845  cbvdisjvw2  36855  mh-setind  37155  regsfromregtco  37157  regsfromsetind  37158  regsfromunir1  37159  mh-prprimbi  37162  mh-unprimbi  37163  mh-infprim1bi  37165  mh-infprim2bi  37166  mh-infprim3bi  37167  bj-notalbii  37330  bj-cbvaew  37374  bj-ssbeq  37383  bj-ax12ssb  37388  bj-nfalt  37446  bj-substax12  37457  bj-nnfalt  37523  bj-nnfext  37524  ax11-pm2  37579  bj-sblem  37587  eliminable-veqab  37609  eliminable-abeqv  37610  eliminable-abeqab  37611  bj-ralvw  37622  bj-sbeq  37644  bj-nfcf  37666  bj-snsetex  37707  bj-rcleqf  37769  bj-clex  37775  bj-rep  37818  bj-axseprep  37819  fvineqsneq  38166  wl-equsalvw  38301  wl-equsalcom  38306  wl-sb9v  38312  wl-sb8eft  38314  wl-sb8et  38316  wl-2sb6d  38321  wl-alanbii  38332  wl-sb8eut  38341  wl-sb8eutv  38342  poimirlem25  38394  poimirlem30  38399  heibor1lem  38559  sbcalfi  38864  mpobi123f  38910  mptbi12f  38914  ineccnvmo  39105  alrmomorn  39106  ralmo  39108  ralrmo3  39112  cocossss  39274  cossssid3  39307  cossssid4  39308  cosscnvssid4  39315  trcoss2  39322  dfeldisj4  39560  dfeldisj5  39561  disjres  39592  dvelimf-o  39802  axc11n-16  39811  pmapglbx  40642  sn-axrep5v  43087  abbibw  43523  dford4  43870  unielss  44059  onsupmaxb  44080  rp-fakeinunass  44355  rababg  44414  elmapintrab  44416  elinintrab  44417  undmrnresiss  44444  clss2lem  44451  cotrintab  44454  elintima  44493  relexp0eq  44541  dfhe3  44615  snhesn  44626  psshepw  44628  dffrege76  44779  frege77  44780  frege110  44813  dffrege115  44818  frege116  44819  frege118  44821  frege131  44834  ntrneikb  44934  ismnuprim  45118  rr-grothprimbi  45119  ismnushort  45125  rr-grothshortbi  45127  pm10.541  45191  pm10.542  45192  19.21vv  45200  19.31vv  45208  19.28vv  45210  pm11.62  45218  axc11next  45230  pm13.196a  45238  2sbc6g  45239  elnev  45261  hbexgVD  45728  dfac5prim  45813  permaxext  45828  permaxrep  45829  permaxpow  45832  permac8prim  45837  rabssf  45951  sinnpoly  47759  2rexsb  47989  dfich2  48358  ichal  48366  spr0nelg  48376  mo0sn  49744  dffun3f  50608  setrec1lem2  50614  setrec2  50621  setis  50624  alimp-surprise  50709  alimp-no-surprise  50710  dfrals2  50719  alsbii  50729  dfralseu2  50752  alseubii  50761  dfalseu2  50765