Theorem albii 1823

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

Syntax hints:   ↔ wb 205  ∀wal 1537

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

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  2albii  1824  hbxfrbi  1828  alex  1829  2nalexn  1831  2exnaln  1832  imnang  1845  alexn  1848  nfnbiOLD  1859  19.26-2  1875  19.26-3an  1876  19.43OLD  1887  albiim  1893  2albiim  1894  empty  1910  19.32v  1944  19.31v  1945  19.23vv  1947  pm11.53v  1948  19.12vvv  1993  equsalvw  2008  2sb6  2090  sbrimvlem  2095  sbcom3vv  2100  alrot3  2159  alrot4  2160  sbal  2161  sbalv  2162  19.21-2  2205  19.32  2229  19.31  2230  equsalv  2262  sbn  2280  aaan  2332  pm11.53  2346  19.12vv  2347  sbievg  2361  equsal  2417  2sb6rf  2473  sbcom3  2510  sb8eulem  2598  eu1  2612  2mo2  2649  2eu1  2652  2eu1v  2653  2eu3  2655  euae  2661  nulmo  2714  abeq2w  2816  hblem  2869  hblemg  2870  abeq2  2871  abeq1  2872  abbiOLD  2879  nfcriOLD  2896  nfcriOLDOLD  2897  nfcriiOLD  2899  nfceqi  2903  abeq2f  2939  ralbii2  3088  r19.21v  3100  r2allem  3123  r3al  3125  r19.21t  3137  nfra2wOLD  3152  ralcom4  3161  ralcom4OLD  3162  r19.23t  3241  rabid2  3307  rabid2f  3308  rabbi  3309  moel  3349  eqv  3431  eqvf  3432  abv  3433  abvALT  3434  ralv  3446  ceqsralt  3453  ceqsalv  3457  rspc2gv  3561  ralxpxfr2d  3568  clel2g  3581  clel4g  3586  elabgt  3596  elabg  3600  ralab  3621  ralabOLD  3622  ralrab2  3629  euind  3654  reu2  3655  reu3  3657  rmo4  3660  reu8  3663  rmo3f  3664  rmoim  3670  2reuswap  3676  2reuswap2  3677  reuind  3683  2reu5lem2  3686  2reu5lem3  3687  2rmoswap  3691  rmo2  3816  rmo3  3818  rmoanim  3823  dfss2  3903  dfss2OLD  3904  ss2ab  3989  ss2rab  4000  rabss  4001  uniiunlem  4015  dfdif3  4045  ssequn1  4110  unss  4114  ralunb  4121  ssin  4161  vn0  4269  eq0f  4271  eq0  4274  eq0ALT  4275  ssdif0  4294  inssdif0  4300  ab0w  4304  ab0  4305  ab0OLD  4306  ab0ALT  4307  ab0orv  4309  eq0rdv  4335  disj  4378  disjOLD  4379  disj3  4384  ssundif  4415  ralidmw  4435  ralidm  4439  ralf0  4441  ralf0OLD  4445  pwss  4555  rabsssn  4600  ralsnsg  4601  ralsng  4606  disjsn  4644  snssg  4715  pwpw0  4743  pwsnOLD  4829  dfnfc2  4860  unissb  4870  elintrab  4888  ssintrab  4899  intun  4908  intprg  4909  intprOLD  4911  dfiin2g  4958  iunssf  4970  iunss  4971  dfdisj2  5037  cbvdisj  5045  disjor  5050  dftr2  5189  dftr5  5190  axrep1  5206  axrep5  5211  axrep6  5212  axsepgfromrep  5216  axnulALT  5223  vnex  5233  inex1  5236  axpweq  5282  zfpow  5284  axpow2  5285  axpow3  5286  nfnid  5293  dtruALT  5306  reusv2lem4  5319  zfpair2  5348  dtruALT2  5353  ssextss  5363  moabex  5368  dffr6  5538  dffr2  5544  dffr2ALT  5545  dfepfr  5565  frinxp  5660  ssrel2  5685  eqrelrel  5696  reliun  5715  raliunxp  5737  relop  5748  dmopab3  5817  dm0rn0  5823  reldm0  5826  iresn0n0  5952  dffr3  5996  cotrg  6005  idrefALT  6007  asymref  6010  asymref2  6011  intirr  6012  dffr4  6211  sucel  6324  sb8iota  6388  dffun2  6428  dffun3  6429  dffun4  6430  dffun5  6431  dffun6f  6432  dffun7  6445  funopab  6453  funcnv2  6486  funcnv  6487  fun2cnv  6489  fun11  6492  fununi  6493  fnres  6543  mptfnf  6552  fnopabg  6554  brprcneu  6747  fvprc  6748  dffv2  6845  fvn0ssdmfun  6934  dff13  7109  eqoprab2bw  7323  eqoprab2b  7324  mpo2eqb  7384  ralrnmpo  7390  zfun  7567  uniex2  7569  funcnvuni  7752  dfer2  8457  fiint  9021  marypha1lem  9122  marypha2lem3  9126  inf2  9311  axinf2  9328  scottexs  9576  scott0s  9577  aceq1  9804  dfac4  9809  dfac7  9819  dfac0  9820  dfac1  9821  dfac10  9824  dfac10c  9825  dfac10b  9826  kmlem4  9840  kmlem12  9848  kmlem14  9850  kmlem15  9851  kmlem16  9852  dfackm  9853  ac6n  10172  axpowndlem3  10286  zfcndrep  10301  zfcndun  10302  zfcndpow  10303  axgroth5  10511  axgroth2  10512  axgroth4  10519  grothprim  10521  sstskm  10529  fimaxre3  11851  infm3  11864  nnwos  12584  cotr2g  14615  brtrclfv  14641  trclfvcotr  14648  rpnnen2lem12  15862  isprm2  16315  vdwmc2  16608  pgpfac1  19598  pgpfac  19602  iunocv  20798  2ndcdisj2  22516  hausdiag  22704  rnelfmlem  23011  alexsubALTlem3  23108  cnextfun  23123  itg2leub  24804  mptelee  27166  nmoubi  29035  nmobndseqi  29042  nmobndseqiALT  29043  isch2  29486  isch3  29504  choc0  29589  nmopub  30171  nmfnleub  30188  xfree2  30708  nelbOLDOLD  30718  mo5f  30738  nmo  30739  reuxfrdf  30740  rabeqsnd  30749  inpr0  30781  cbvdisjf  30811  disjorf  30819  ssrelf  30856  funcnvmpt  30906  funcnv5mpt  30907  ballotlem2  32355  bnj89  32600  bnj115  32604  bnj1143  32670  bnj110  32738  bnj611  32798  bnj864  32802  bnj865  32803  bnj1000  32821  bnj978  32829  bnj1049  32854  bnj1052  32855  bnj1090  32859  bnj1030  32867  bnj1133  32869  bnj1171  32880  bnj1172  32881  bnj1174  32883  bnj1176  32885  bnj1204  32892  bnj1253  32897  bnj1388  32913  bnj1523  32951  fineqvrep  32964  fineqvpow  32965  axrepprim  33543  axunprim  33544  axpowprim  33545  axinfprim  33547  axacprim  33548  untuni  33550  fnssintima  33578  ralxp3f  33588  dffr5  33627  elintfv  33644  dfon2lem8  33672  dfon2lem9  33673  19.12b  33683  ttrclss  33706  frpoins3xpg  33714  frpoins3xp3g  33715  eqscut2  33927  brtxpsd3  34125  dfom5b  34141  dffun10  34143  bj-notalbii  34723  bj-ssbeq  34761  bj-ax12ssb  34766  bj-hbext  34819  bj-nfalt  34820  bj-substax12  34830  bj-nnfalt  34875  bj-nnfext  34876  ax11-pm2  34946  bj-sbnf  34951  bj-sblem  34955  eliminable-veqab  34977  eliminable-abeqv  34978  eliminable-abeqab  34979  bj-ralvw  34991  bj-sbeq  35013  bj-nfcf  35038  bj-snsetex  35080  bj-rcleqf  35142  fvineqsneq  35510  wl-equsalvw  35624  wl-equsalcom  35628  wl-sb8et  35635  wl-2sb6d  35640  wl-alanbii  35651  wl-sb8eut  35659  poimirlem25  35729  poimirlem30  35734  heibor1lem  35894  sbcalfi  36201  mpobi123f  36247  mptbi12f  36251  3albii  36314  ineccnvmo  36416  alrmomorn  36417  cocossss  36486  cossssid3  36514  cossssid4  36515  cosscnvssid4  36522  trcoss2  36529  dfeldisj4  36758  dfeldisj5  36759  dvelimf-o  36870  axc11n-16  36879  pmapglbx  37710  sn-axrep5v  40113  dford4  40767  rp-fakeinunass  41020  rababg  41070  elmapintrab  41073  elinintrab  41074  undmrnresiss  41101  clss2lem  41108  cotrintab  41111  elintima  41150  ss2iundf  41156  relexp0eq  41198  dfhe3  41272  snhesn  41283  psshepw  41285  dffrege76  41436  frege77  41437  frege110  41470  dffrege115  41475  frege116  41476  frege118  41478  frege131  41491  ntrneikb  41593  ismnuprim  41801  rr-grothprimbi  41802  ismnushort  41808  rr-grothshortbi  41810  pm10.541  41874  pm10.542  41875  19.21vv  41883  19.31vv  41891  19.28vv  41893  pm11.62  41901  axc11next  41913  pm13.196a  41921  2sbc6g  41922  elnev  41945  hbexgVD  42415  rabssf  42557  2rexsb  44480  dfich2  44798  ichal  44806  spr0nelg  44816  mo0sn  46049  dffun3f  46274  setrec1lem2  46280  setrec2  46287  setis  46289  alimp-surprise  46370  alimp-no-surprise  46371