Theorem albii 1782

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

Syntax hints:   ↔ wb 198  ∀wal 1505

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

This theorem depends on definitions:  df-bi 199

This theorem is referenced by:  2albii  1783  hbxfrbi  1787  alex  1788  2nalexn  1790  2exnaln  1791  imnang  1804  alexn  1807  nfnbi  1817  19.26-2  1834  19.26-3an  1835  19.43OLD  1846  albiim  1852  2albiim  1853  19.32v  1899  19.31v  1900  19.23vv  1902  pm11.53v  1903  19.12vvv  1945  equsalvw  1961  sbcom3vv  2042  alrot3  2096  alrot4  2097  19.21-2  2138  19.23tOLD  2140  19.32  2165  19.31  2166  equsalv  2196  2sb6  2211  sbn  2214  aaan  2273  pm11.53  2280  19.12vv  2281  equsal  2352  2sb6rf  2419  2sb6rfOLD  2420  sbcom3  2472  sbal  2499  sbex  2501  sbalv  2502  eu6OLDOLD  2593  sb8eulem  2631  eu1  2640  eu1OLD  2641  2mo2  2678  2eu1  2681  2eu1OLD  2682  2eu3  2684  2eu3OLD  2685  euae  2691  euaeOLD  2692  nulmo  2756  nulmoOLD  2757  hblem  2896  abeq2  2897  abeq1  2898  abbi  2907  nfcrii  2925  nfceqi  2928  abeq2f  2964  abeq2fOLD  2965  ralbii2  3113  ralanidOLD  3119  r19.21v  3125  r2allem  3150  r3al  3152  r19.21t  3164  ralcom4  3182  r19.23t  3256  rabid2  3320  rabid2f  3321  rabbi  3322  eqv  3423  eqvf  3424  abv  3425  ralv  3440  ceqsralt  3449  rspc2gv  3547  ralxpxfr2d  3554  ralab  3600  ralrab2  3605  euind  3627  reu2  3628  reu3  3630  rmo4  3633  reu8  3636  rmo3f  3637  rmoim  3643  2reuswap  3649  2reuswap2  3650  reuind  3653  2reu5lem2  3656  2reu5lem3  3657  2rmoswap  3661  rmo2  3773  rmo3  3775  rmo3OLD  3776  rmoanim  3781  dfss2  3846  ss2ab  3929  ss2rab  3937  rabss  3938  uniiunlem  3951  dfdif3  3981  ssequn1  4044  unss  4048  ralunb  4055  ssin  4094  eq0f  4191  ssdif0  4209  inssdif0  4215  ab0  4219  disj  4282  disj3  4286  ssundif  4316  ralf0  4340  pwss  4439  rabsssn  4479  ralsnsg  4480  disjsn  4521  snssg  4591  pwpw0  4620  pwsnALT  4705  dfnfc2  4730  unissb  4743  elintrab  4761  ssintrab  4772  intun  4781  intpr  4782  dfiin2g  4827  iunss  4835  dfdisj2  4899  cbvdisj  4907  disjor  4911  dftr2  5032  dftr5  5033  trintOLD  5047  axrep1  5050  axrep5  5055  axsep  5059  axnulALT  5065  vnex  5075  inex1  5078  axpweq  5118  zfpow  5120  axpow2  5121  axpow3  5122  nfnid  5129  dtruALT  5141  reusv2lem4  5155  zfpair2  5187  dtruALT2  5192  ssextss  5203  moabex  5208  dffr2  5372  dfepfr  5392  frinxp  5484  ssrel2  5509  eqrelrel  5520  reliun  5539  raliunxp  5560  relop  5571  dmopab3  5635  dm0rn0  5640  reldm0  5641  dffr3  5802  cotrg  5811  idrefALT  5813  asymref  5816  asymref2  5817  intirr  5818  dffr4  6002  sucel  6102  sb8iota  6159  dffun2  6198  dffun3  6199  dffun4  6200  dffun5  6201  dffun6f  6202  dffun7  6215  funopab  6223  funcnv2  6255  funcnv  6256  fun2cnv  6258  fun11  6261  fununi  6262  fnres  6306  mptfnf  6313  fnopabg  6315  brprcneu  6491  dffv2  6584  fvn0ssdmfun  6667  dff13  6838  eqoprab2b  7043  mpo2eqb  7099  ralrnmpo  7105  zfun  7280  uniex2  7282  funcnvuni  7451  dfer2  8090  fiint  8590  marypha1lem  8692  marypha2lem3  8696  inf2  8880  axinf2  8897  scottexs  9110  scott0s  9111  aceq1  9337  dfac4  9342  dfac7  9352  dfac0  9353  dfac1  9354  dfac10  9357  dfac10c  9358  dfac10b  9359  kmlem4  9373  kmlem12  9381  kmlem14  9383  kmlem15  9384  kmlem16  9385  dfackm  9386  ac6n  9705  axpowndlem3  9819  zfcndrep  9834  zfcndun  9835  zfcndpow  9836  axgroth5  10044  axgroth2  10045  axgroth4  10052  grothprim  10054  sstskm  10062  fimaxre3  11388  infm3  11401  nnwos  12129  cotr2g  14197  brtrclfv  14223  trclfvcotr  14230  rpnnen2lem12  15438  isprm2  15882  vdwmc2  16171  pgpfac1  18952  pgpfac  18956  iunocv  20527  2ndcdisj2  21769  hausdiag  21957  rnelfmlem  22264  alexsubALTlem3  22361  cnextfun  22376  itg2leub  24038  mptelee  26384  nmoubi  28326  nmobndseqi  28333  nmobndseqiALT  28334  isch2  28779  isch3  28797  choc0  28884  nmopub  29466  nmfnleub  29483  xfree2  30003  moel  30034  mo5f  30035  nmo  30036  rabeqsnd  30043  cbvdisjf  30088  disjorf  30095  ssrelf  30130  funcnvmpt  30174  funcnv5mpt  30175  ballotlem2  31398  bnj89  31645  bnj115  31649  bnj1143  31716  bnj110  31783  bnj611  31843  bnj864  31847  bnj865  31848  bnj1000  31866  bnj978  31874  bnj1049  31897  bnj1052  31898  bnj1090  31902  bnj1030  31910  bnj1133  31912  bnj1171  31923  bnj1172  31924  bnj1174  31926  bnj1176  31928  bnj1204  31935  bnj1253  31940  bnj1388  31956  bnj1523  31994  axrepprim  32454  axunprim  32455  axpowprim  32456  axinfprim  32458  axacprim  32459  untuni  32461  dffr5  32515  elintfv  32533  dfon2lem8  32561  dfon2lem9  32562  19.12b  32573  brtxpsd3  32884  dfom5b  32900  dffun10  32902  bj-notalbii  33470  bj-ssbeq  33500  bj-ax12ssb  33505  bj-hbext  33560  bj-nfalt  33561  bj-abeq2  33611  bj-abeq1  33612  bj-axrep1  33624  bj-axrep5  33628  bj-axsep  33629  ax11-pm2  33656  bj-sbnf  33661  bj-sblem  33665  bj-ralvw  33694  bj-sbeq  33716  bj-nfcf  33742  bj-nnfalt  33797  bj-nnfext  33798  bj-snsetex  33799  fvineqsneq  34140  wl-equsalvw  34226  wl-equsalcom  34230  wl-sb8et  34236  wl-2sb6d  34241  wl-alanbii  34252  wl-sb8eut  34260  wl-dfralsb  34284  wl-dfralflem  34285  wl-dfralv  34288  wl-dfrexex  34297  wl-dfrexsb  34298  wl-dfrmosb  34300  wl-dfrmov  34301  poimirlem25  34364  poimirlem30  34369  heibor1lem  34535  sbcalfi  34844  mpobi123f  34890  mptbi12f  34894  3albii  34959  ineccnvmo  35063  alrmomorn  35064  cocossss  35132  cossssid3  35160  cossssid4  35161  cosscnvssid4  35168  trcoss2  35175  dfeldisj4  35404  dfeldisj5  35405  dvelimf-o  35516  axc11n-16  35525  pmapglbx  36356  sn-axrep  38558  sn-axrep5v  38559  dford4  39028  rp-fakeinunass  39283  rababg  39301  elmapintrab  39304  elinintrab  39305  undmrnresiss  39332  clss2lem  39340  cotrintab  39343  elintima  39367  ss2iundf  39373  relexp0eq  39415  dfhe3  39490  snhesn  39501  psshepw  39503  dffrege76  39654  frege77  39655  frege110  39688  dffrege115  39693  frege116  39694  frege118  39696  frege131  39709  ntrneikb  39813  ntrneixb  39814  ismnuprim  40011  rr-grothprimbi  40012  pm10.541  40121  pm10.542  40122  19.21vv  40130  19.31vv  40138  19.28vv  40140  pm11.62  40149  axc11next  40161  pm13.196a  40169  2sbc6g  40170  elnev  40193  hbexgVD  40665  iunssf  40779  rabssf  40814  2rexsb  42711  dfich2  42989  dfich2ai  42990  ichal  43003  spr0nelg  43012  dffun3f  44158  setrec1lem2  44164  setrec2  44171  setis  44173  alimp-surprise  44254  alimp-no-surprise  44255