MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  albii Structured version   Visualization version   GIF version

Theorem albii 1904
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
StepHypRef Expression
1 albi 1903 . 2 (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ↔ ∀𝑥𝜓))
2 albii.1 . 2 (𝜑𝜓)
31, 2mpg 1879 1 (∀𝑥𝜑 ↔ ∀𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 197  wal 1635
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894
This theorem depends on definitions:  df-bi 198
This theorem is referenced by:  2albii  1905  hbxfrbi  1909  alex  1910  2nalexn  1912  2exnaln  1913  imnang  1928  alexn  1930  nfnbi  1940  nfnbiOLD  1941  19.26-2  1960  19.26-3an  1961  19.26-3anOLD  1962  19.43OLD  1973  albiim  1978  2albiim  1979  nfbiiOLD  1998  19.32v  2032  19.31v  2033  19.23vv  2035  pm11.53v  2086  19.12vvv  2087  equsalvw  2101  alrot3  2206  alrot4  2207  19.21-2  2246  19.23t  2247  19.32  2270  19.31  2271  equsalv  2277  2sb6  2291  equsalhwOLD  2301  aaan  2345  pm11.53  2355  19.12vv  2356  19.21-2OLD  2391  19.23tOLD  2394  equsal  2460  sbcom3  2572  2sb6rf  2615  sbex  2626  sbalv  2627  eu6  2641  sb8eu  2673  eu1  2680  2mo2  2721  2eu1  2724  2eu3  2726  exists1  2732  nulmo  2798  hblem  2922  abeq2  2923  abeq1  2924  abbi  2928  abeq2f  2983  ralanid  3113  r2allem  3132  r3al  3135  r19.21t  3150  r19.21v  3155  ralbii2  3173  r19.23t  3216  rabid2  3314  rabid2f  3315  rabbi  3316  eqv  3404  eqvf  3405  abv  3407  ralv  3420  ceqsralt  3430  rspc2gv  3521  ralxpxfr2d  3528  ralab  3570  ralrab2  3575  euind  3598  reu2  3599  reu3  3601  rmo4  3604  reu8  3607  rmoim  3612  2reuswap  3615  reuind  3616  2reu5lem2  3619  2reu5lem3  3620  rmo2  3728  rmo3  3730  dfss2  3793  ss2ab  3874  ss2rab  3882  rabss  3883  uniiunlem  3896  dfdif3  3926  ssequn1  3989  unss  3993  ralunb  4000  ssin  4038  eq0f  4134  ssdif0  4150  inssdif0  4155  ab0  4159  disj  4221  disj3  4225  ssundif  4255  ralf0  4279  pwss  4375  rabsssn  4415  ralsnsg  4416  disjsn  4445  euabsn2  4458  snssg  4512  pwpw0  4541  pwsnALT  4630  dfnfc2  4657  unissb  4670  elintrab  4688  ssintrab  4699  intun  4708  intpr  4709  dfiin2g  4752  iunss  4760  dfdisj2  4821  cbvdisj  4829  disjor  4833  dftr2  4955  dftr5  4956  trint  4968  axrep1  4972  axrep5  4977  axsep  4981  zfnuleuOLD  4987  axnulALT  4988  vnex  4998  inex1  5001  axpweq  5041  zfpow  5043  axpow2  5044  axpow3  5045  nfnid  5052  dtruALT  5064  reusv2lem4  5077  zfpair2  5104  dtruALT2  5108  ssextss  5119  moabex  5124  dffr2  5283  dfepfr  5303  frinxp  5393  ssrelOLD  5417  ssrel2  5419  eqrelrel  5430  reliun  5448  raliunxp  5470  relop  5481  dmopab3  5545  dm0rn0  5550  reldm0  5551  dffr3  5715  cotrg  5724  idrefALT  5726  idrefOLD  5727  asymref  5730  asymref2  5731  intirr  5732  dffr4  5916  sucel  6017  sb8iota  6074  dffun2  6114  dffun3  6115  dffun4  6116  dffun5  6117  dffun6f  6118  dffun7  6131  funopab  6139  funcnv2  6171  funcnv  6172  fun2cnv  6174  fun11  6177  fununi  6178  fnres  6221  mptfnf  6229  fnopabg  6231  brprcneu  6403  dffv2  6495  fvn0ssdmfun  6575  dff13  6739  eqoprab2b  6946  mpt22eqb  7002  ralrnmpt2  7008  zfun  7183  uniex2  7185  funcnvuni  7352  dfer2  7983  fiint  8479  marypha1lem  8581  marypha2lem3  8585  inf2  8770  axinf2  8787  scottexs  9000  scott0s  9001  aceq1  9226  dfac4  9231  dfac7  9242  dfac0  9243  dfac1  9244  dfac10  9247  dfac10c  9248  dfac10b  9249  kmlem4  9263  kmlem12  9271  kmlem14  9273  kmlem15  9274  kmlem16  9275  dfackm  9276  ac6n  9595  axpowndlem3  9709  zfcndrep  9724  zfcndun  9725  zfcndpow  9726  axgroth5  9934  axgroth2  9935  grothpw  9936  axgroth4  9942  grothprim  9944  sstskm  9952  fimaxre3  11258  infm3  11270  nnwos  11977  cotr2g  13943  brtrclfv  13969  trclfvcotr  13976  rpnnen2lem12  15177  isprm2  15616  vdwmc2  15903  pgpfac1  18684  pgpfac  18688  iunocv  20239  2ndcdisj2  21478  hausdiag  21666  rnelfmlem  21973  alexsubALTlem3  22070  cnextfun  22085  itg2leub  23721  mptelee  25995  nmoubi  27961  nmobndseqi  27968  nmobndseqiALT  27969  isch2  28414  isch3  28432  choc0  28519  nmopub  29101  nmfnleub  29118  xfree2  29638  moel  29657  mo5f  29658  nmo  29659  2reuswap2  29660  rmo3f  29667  rmo4fOLD  29668  rabeqsnd  29673  cbvdisjf  29716  disjorf  29723  ssrelf  29758  funcnvmptOLD  29800  funcnvmpt  29801  funcnv5mpt  29802  ballotlem2  30881  bnj89  31118  bnj115  31122  bnj1143  31189  bnj110  31256  bnj611  31316  bnj864  31320  bnj865  31321  bnj1000  31339  bnj978  31347  bnj1049  31370  bnj1052  31371  bnj1090  31375  bnj1030  31383  bnj1133  31385  bnj1171  31396  bnj1172  31397  bnj1174  31399  bnj1176  31401  bnj1204  31408  bnj1253  31413  bnj1388  31429  bnj1523  31467  axrepprim  31906  axunprim  31907  axpowprim  31908  axinfprim  31910  axacprim  31911  untuni  31913  dffr5  31970  elintfv  31989  dfon2lem8  32020  dfon2lem9  32021  19.12b  32032  brtxpsd3  32329  dfom5b  32345  dffun10  32347  bj-notalbii  32918  bj-ssbeq  32948  bj-ssb0  32949  bj-ssb1a  32953  bj-ssb1  32954  bj-ax12ssb  32956  bj-ssbn  32961  bj-ssbcom3lem  32970  bj-hbext  33021  bj-nfalt  33022  bj-abeq2  33089  bj-abeq1  33090  bj-axrep1  33104  bj-axrep5  33108  bj-axsep  33109  bj-zfpow  33111  ax11-pm2  33138  bj-sbnf  33143  bj-ralvw  33175  bj-ralcom4  33178  bj-sbeq  33206  bj-nfcf  33232  bj-snsetex  33263  bj-raldifsn  33367  wl-equsalcom  33644  wl-sb8et  33651  wl-2sb6d  33657  wl-alanbii  33667  wl-sb8eut  33675  poimirlem25  33749  poimirlem30  33754  heibor1lem  33921  sbcalfi  34232  mpt2bi123f  34283  mptbi12f  34287  3albii  34333  ineccnvmo  34437  alrmomorn  34438  cocossss  34506  cossssid3  34534  cossssid4  34535  cosscnvssid4  34542  trcoss2  34549  dvelimf-o  34710  axc11n-16  34719  pmapglbx  35551  dford4  38098  rp-fakeinunass  38362  rababg  38380  elmapintrab  38383  elinintrab  38384  undmrnresiss  38411  clss2lem  38419  cotrintab  38422  elintima  38446  ss2iundf  38452  relexp0eq  38494  dfhe3  38570  snhesn  38581  psshepw  38583  dffrege76  38734  frege77  38735  frege110  38768  dffrege115  38773  frege116  38774  frege118  38776  frege131  38789  ntrneikb  38893  ntrneixb  38894  pm10.541  39067  pm10.542  39068  19.21vv  39076  19.31vv  39084  19.28vv  39086  pm11.62  39095  axc11next  39107  pm13.196a  39115  2sbc6g  39116  elnev  39139  hbexgVD  39637  iunssf  39757  rabssf  39795  2rexsb  41684  2rmoswap  41697  spr0nelg  42295  dffun3f  42998  setrec1lem2  43004  setrec2  43011  setis  43013  alimp-surprise  43098  alimp-no-surprise  43099
  Copyright terms: Public domain W3C validator