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

Theorem albii 1787
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 1786 . 2 (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ↔ ∀𝑥𝜓))
2 albii.1 . 2 (𝜑𝜓)
31, 2mpg 1764 1 (∀𝑥𝜑 ↔ ∀𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wal 1521
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777
This theorem depends on definitions:  df-bi 197
This theorem is referenced by:  2albii  1788  hbxfrbi  1792  alex  1793  2nalexn  1795  2exnaln  1796  imnang  1809  alexn  1811  nfnbi  1821  19.26-2  1839  19.26-3an  1840  19.43OLD  1851  albiim  1856  2albiim  1857  nfbiiOLD  1876  19.32v  1909  19.31v  1910  19.23vv  1912  pm11.53v  1962  19.12vvv  1963  equsalvw  1977  alrot3  2078  alrot4  2079  19.21-2  2116  19.23t  2117  19.32  2139  19.31  2140  equsalv  2146  equsalhw  2161  aaan  2206  pm11.53  2215  19.12vv  2216  19.21-2OLD  2251  19.23tOLD  2254  equsal  2327  sbcom3  2439  2sb6  2472  2sb6rf  2480  sbex  2491  sbalv  2492  sb8eu  2532  eu1  2539  2mo2  2579  2eu1  2582  2eu3  2584  exists1  2590  hblem  2760  abeq2  2761  abeq1  2762  abbi  2766  abeq2f  2821  r2allem  2966  r3al  2969  r19.21t  2984  r19.21v  2989  ralbii2  3007  r19.23t  3050  rabid2  3148  rabid2f  3149  rabbi  3150  eqvf  3235  abv  3237  ralv  3250  ceqsralt  3260  rspc2gv  3352  ralxpxfr2d  3358  ralab  3400  ralrab2  3405  euind  3426  reu2  3427  reu3  3429  rmo4  3432  reu8  3435  rmoim  3440  2reuswap  3443  reuind  3444  2reu5lem2  3447  2reu5lem3  3448  rmo2  3559  rmo3  3561  dfss2  3624  ss2ab  3703  ss2rab  3711  rabss  3712  uniiunlem  3724  ssequn1  3816  unss  3820  ralunb  3827  ssin  3868  eq0f  3958  n0fOLD  3961  ssdif0  3975  inssdif0  3980  ab0  3984  disj  4050  disj3  4054  ssundif  4085  ralf0  4111  pwss  4208  rabsssn  4247  ralsnsg  4248  disjsn  4278  euabsn2  4292  snssg  4347  pwpw0  4376  pwsnALT  4461  dfnfc2  4486  dfnfc2OLD  4487  unissb  4501  elintrab  4520  ssintrab  4532  intun  4541  intpr  4542  dfiin2g  4585  iunss  4593  dfdisj2  4654  cbvdisj  4662  disjor  4666  dftr2  4787  dftr5  4788  trint  4801  axrep1  4805  axrep5  4809  axsep  4813  zfnuleu  4819  axnulALT  4820  vprc  4829  inex1  4832  axpweq  4872  zfpow  4874  axpow2  4875  axpow3  4876  reusv2lem4  4902  nfnid  4927  dtruALT  4929  zfpair2  4937  dtruALT2  4941  ssextss  4952  moabex  4957  dffr2  5108  dfepfr  5128  frinxp  5218  ssrelOLD  5242  ssrel2  5244  eqrelrel  5255  reliun  5272  raliunxp  5294  relop  5305  dmopab3  5369  dm0rn0  5374  reldm0  5375  dffr3  5533  cotrg  5542  issref  5544  asymref  5547  asymref2  5548  intirr  5549  dffr4  5734  sucel  5836  sb8iota  5896  dffun2  5936  dffun3  5937  dffun4  5938  dffun5  5939  dffun6f  5940  dffun7  5953  funopab  5961  funcnv2  5995  funcnv  5996  fun2cnv  5998  fun11  6001  fununi  6002  fnres  6045  mptfnf  6053  fnopabg  6055  brprcneu  6222  dffv2  6310  fvn0ssdmfun  6390  dff13  6552  eqoprab2b  6755  mpt22eqb  6811  ralrnmpt2  6817  zfun  6992  uniex2  6994  funcnvuni  7161  dfer2  7788  fiint  8278  marypha1lem  8380  marypha2lem3  8384  inf2  8558  axinf2  8575  scottexs  8788  scott0s  8789  aceq1  8978  dfac4  8983  dfac7  8992  dfac0  8993  dfac1  8994  dfac10  8997  dfac10c  8998  dfac10b  8999  kmlem4  9013  kmlem12  9021  kmlem14  9023  kmlem15  9024  kmlem16  9025  dfackm  9026  ac6n  9345  axpowndlem3  9459  zfcndrep  9474  zfcndun  9475  zfcndpow  9476  axgroth5  9684  axgroth2  9685  grothpw  9686  axgroth4  9692  grothprim  9694  sstskm  9702  fimaxre3  11008  infm3  11020  nnwos  11793  cotr2g  13761  brtrclfv  13787  trclfvcotr  13794  rpnnen2lem12  14998  isprm2  15442  vdwmc2  15730  pgpfac1  18525  pgpfac  18529  iunocv  20073  2ndcdisj2  21308  hausdiag  21496  rnelfmlem  21803  alexsubALTlem3  21900  cnextfun  21915  itg2leub  23546  mptelee  25820  nmoubi  27755  nmobndseqi  27762  nmobndseqiALT  27763  isch2  28208  isch3  28226  choc0  28313  nmopub  28895  nmfnleub  28912  xfree2  29432  moel  29451  mo5f  29452  nmo  29453  2reuswap2  29455  rmo3f  29462  rmo4fOLD  29463  rabeqsnd  29468  cbvdisjf  29511  disjorf  29518  ssrelf  29553  funcnvmptOLD  29595  funcnvmpt  29596  funcnv5mpt  29597  ballotlem2  30678  bnj89  30915  bnj115  30919  bnj538OLD  30936  bnj1143  30987  bnj110  31054  bnj611  31114  bnj864  31118  bnj865  31119  bnj1000  31137  bnj978  31145  bnj1049  31168  bnj1052  31169  bnj1090  31173  bnj1030  31181  bnj1133  31183  bnj1171  31194  bnj1172  31195  bnj1174  31197  bnj1176  31199  bnj1204  31206  bnj1253  31211  bnj1388  31227  bnj1523  31265  axrepprim  31705  axunprim  31706  axpowprim  31707  axinfprim  31709  axacprim  31710  untuni  31712  dffr5  31769  elintfv  31788  dfon2lem8  31819  dfon2lem9  31820  19.12b  31831  brtxpsd3  32128  dfom5b  32144  dffun10  32146  bj-notalbii  32723  bj-ssbeq  32752  bj-ssb0  32753  bj-ssb1a  32757  bj-ssb1  32758  bj-ax12ssb  32760  bj-ssbn  32766  bj-ssbcom3lem  32775  bj-hbext  32826  bj-nfalt  32827  bj-abeq2  32898  bj-abeq1  32899  bj-axrep1  32913  bj-axrep5  32917  bj-axsep  32918  bj-zfpow  32920  ax11-pm2  32948  bj-sbnf  32953  bj-hblem  32974  bj-ralvw  32990  bj-ralcom4  32993  bj-sbeq  33021  bj-nfcf  33045  bj-snsetex  33076  bj-raldifsn  33179  wl-equsalcom  33458  wl-sb8et  33464  wl-2sb6d  33471  wl-alanbii  33481  wl-sb8eut  33489  wl-sbcom3  33502  poimirlem25  33564  poimirlem30  33569  heibor1lem  33738  sbcalfi  34049  mpt2bi123f  34101  mptbi12f  34105  ralanid  34152  3albii  34154  ineccnvmo  34262  alrmomorn  34263  cocossss  34331  cossssid3  34359  cossssid4  34360  cosscnvssid4  34367  trcoss2  34374  dvelimf-o  34533  axc11n-16  34542  pmapglbx  35373  dford4  37913  rp-fakeinunass  38178  rababg  38196  elmapintrab  38199  elinintrab  38200  undmrnresiss  38227  clss2lem  38235  cotrintab  38238  elintima  38262  ss2iundf  38268  relexp0eq  38310  dfhe3  38386  snhesn  38397  psshepw  38399  dffrege76  38550  frege77  38551  frege110  38584  dffrege115  38589  frege116  38590  frege118  38592  frege131  38605  ntrneikb  38709  ntrneixb  38710  pm10.541  38883  pm10.542  38884  19.21vv  38892  19.31vv  38900  19.28vv  38902  pm11.62  38911  axc11next  38924  pm13.196a  38932  2sbc6g  38933  elnev  38956  conss34OLD  38963  hbexgVD  39456  iunssf  39577  rabssf  39616  2rexsb  41491  2rmoswap  41505  spr0nelg  42051  dffun3f  42754  setrec1lem2  42760  setrec2  42767  setis  42769  alimp-surprise  42854  alimp-no-surprise  42855
  Copyright terms: Public domain W3C validator