MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exbii Unicode version

Theorem exbii 1589
Description: Inference adding existential quantifier to both sides of an equivalence. (Contributed by NM, 24-May-1994.)
Hypothesis
Ref Expression
exbii.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
exbii  |-  ( E. x ph  <->  E. x ps )

Proof of Theorem exbii
StepHypRef Expression
1 exbi 1588 . 2  |-  ( A. x ( ph  <->  ps )  ->  ( E. x ph  <->  E. x ps ) )
2 exbii.1 . 2  |-  ( ph  <->  ps )
31, 2mpg 1554 1  |-  ( E. x ph  <->  E. x ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 177   E.wex 1547
This theorem is referenced by:  2exbii  1590  3exbii  1591  exanali  1592  exancom  1593  19.43  1612  exiftruOLD  1666  excom  1752  excom13  1754  exrot4  1756  eeor  1903  19.12vv  1917  19.41vv  1921  19.41vvv  1922  19.41vvvv  1923  exdistr  1925  19.42vvv  1927  exdistr2  1928  3exdistr  1929  4exdistrOLD  1931  eean  1932  eeeanv  1934  eeeanvOLD  1935  ee4anv  1936  equsexOLD  1970  2sb5  2161  2sb5rf  2167  sbel2x  2175  exsbOLD  2181  2exsb  2182  sb8eu  2272  eu1  2275  eu2  2279  sbmo  2284  moanim  2310  2moswap  2329  2eu1  2334  exists1  2343  clelab  2524  clabel  2525  sbabel  2566  rexbii2  2695  r2exf  2702  r19.41  2820  isset  2920  rexv  2930  ceqsex2  2952  ceqsex3v  2954  gencbvex  2958  vtocl2  2967  vtocl3  2968  spc3gv  3001  ceqsrexv  3029  rexab  3057  rexrab2  3062  euxfr  3080  euind  3081  reu6  3083  reu3  3084  2reuswap  3096  reuind  3097  2reu5lem3  3101  2reu5  3102  sbccomlem  3191  rmo2  3206  rexun  3487  reupick3  3586  abn0  3606  pssnel  3653  rexsns  3805  exsnrex  3808  snprc  3831  euabsn2  3835  reusn  3837  eusn  3840  elunirab  3988  unipr  3989  uniun  3994  uniin  3995  uni0b  4000  uniintsn  4047  iuncom4  4060  dfiun2g  4083  iunn0  4111  iunxiun  4133  disjor  4156  cbvopab2  4239  cbvopab2v  4242  unopab  4244  axrep1  4281  axrep4  4284  axrep5  4285  zfrep4  4288  axsep  4289  zfnuleu  4295  axnulALT  4296  0ex  4299  vprc  4301  inex1  4304  inuni  4322  axpweq  4336  zfpow  4338  axpow2  4339  axpow3  4340  pwex  4342  zfpair  4361  zfpair2  4364  eqvinop  4401  copsexg  4402  opabn0  4445  iunopab  4446  dfid3  4459  zfun  4661  uniex2  4663  uniuni  4675  reusv5OLD  4692  elxp2  4855  opeliunxp  4888  xpiundi  4891  xpiundir  4892  elvvv  4896  eliunxp  4971  relop  4982  opelco2g  4999  cnvco  5015  cnvuni  5016  dfdm3  5017  dfrn2  5018  dfrn3  5019  elrng  5021  dfdm4  5022  eldm2g  5025  dmun  5035  dmin  5036  dmiun  5037  dmuni  5038  dmopab  5039  dmi  5043  elrn  5069  rnopab  5074  dmcosseq  5096  dmres  5126  elres  5140  elsnres  5141  dfima2  5164  elima3  5169  imadmrn  5174  imai  5177  args  5191  rniun  5241  ssrnres  5268  dmsnn0  5294  dmsnopg  5300  elxp4  5316  elxp5  5317  cnvresima  5318  mptpreima  5322  dfco2  5328  coundi  5330  coundir  5331  resco  5333  imaco  5334  rnco  5335  coiun  5338  coi1  5344  coass  5347  xpco  5373  dffun2  5423  dffun5  5426  imadif  5487  funimaexg  5489  fun11iun  5654  f11o  5667  brprcneu  5680  dffv2  5755  fndmin  5796  fvresex  5941  abrexco  5945  opabex3d  5948  opabex3  5949  imaiun  5951  abexssex  5961  abexex  5962  isomin  6016  dfoprab2  6080  cbvoprab2  6104  oprabrexex2  6148  releldm2  6356  dfopab2  6360  dfoprab3s  6361  exopxfr  6369  fsplit  6410  frxp  6415  brtpos2  6444  oarec  6764  oeeu  6805  domen  7080  mapsnen  7143  xpsnen  7151  xpcomco  7157  xpassen  7161  inf2  7534  zfinf  7550  axinf2  7551  zfinf2  7553  rankuni  7745  scott0  7766  cp  7771  ween  7872  aceq1  7954  aceq0  7955  aceq2  7956  dfac5lem1  7960  dfac5lem2  7961  dfac5lem3  7962  kmlem3  7988  kmlem14  7999  kmlem15  8000  kmlem16  8001  cflem  8082  cf0  8087  cfval2  8096  cfss  8101  cfslb  8102  fin23lem32  8180  axdc2lem  8284  zfac  8296  ac9  8319  ac9s  8329  axpowndlem3  8430  zfcndrep  8445  zfcndun  8446  zfcndpow  8447  zfcndinf  8449  zfcndac  8450  axgroth5  8655  axgroth2  8656  grothpw  8657  axgroth6  8659  axgroth3  8662  axgroth4  8663  grothprim  8665  grothtsk  8666  genpass  8842  ltexprlem1  8869  ltexprlem4  8872  supmul1  9929  supmullem2  9931  2rexuz  10485  nnwos  10500  hashfun  11655  maxprmfct  13068  4sqlem12  13279  vdwmc  13301  imasleval  13721  isacs2  13833  gsumval3eu  15468  lidlnz  16254  isbasis2g  16968  tgval2  16976  ntreq0  17096  lmff  17319  cmpfi  17425  is1stc2  17458  1stcelcls  17477  isfbas2  17820  elfg  17856  alexsubALTlem3  18033  ustfilxp  18195  metrest  18507  metuel2  18562  restmetu  18570  cmetss  19220  dchrvmasumlema  21147  usgraedg4  21359  3v3e3cycl2  21604  isgrpo  21737  ismgm  21861  nmo  23926  2reuswap2  23928  rexunirn  23931  disjorf  23974  axextprim  25103  axrepprim  25104  axunprim  25105  axpowprim  25106  axregprim  25107  axinfprim  25108  axacprim  25109  cbvprod  25194  iprodmul  25269  dftr6  25321  coep  25322  coepr  25323  dffr5  25324  dfpo2  25326  cnvco1  25331  cnvco2  25332  eldm3  25333  fundmpss  25336  dfdm5  25346  dfrn5  25347  domep  25363  axextdfeq  25368  19.12b  25372  axextndbi  25375  wfrlem11  25480  tfrALTlem  25490  frrlem5c  25501  nofulllem5  25574  brtxp  25634  brpprod  25639  brsset  25643  dfon3  25646  brtxpsd  25648  elfix  25657  dffix2  25659  dffun10  25667  elfuns  25668  elsingles  25671  snelsingles  25675  dfiota3  25676  brimg  25690  brapply  25691  brcup  25692  brcap  25693  brsuccf  25694  funpartlem  25695  brrestrict  25702  dfrdg4  25703  tfrqfree  25704  supaddc  26137  supadd  26138  ismblfin  26146  itg2addnclem3  26157  itg2addnc  26158  neifg  26290  prtlem16  26608  prter2  26620  diophrex  26724  19.36vv  27449  19.37vv  27451  pm11.58  27457  pm11.6  27459  pm13.192  27478  2sbc5g  27484  iotasbc2  27488  rfcnnnub  27574  stoweidlem34  27650  stoweidlem35  27651  stoweidlem60  27676  rmoanim  27824  2rmoswap  27829  el2wlkonot  28066  el2spthonot  28067  el2wlkonotot0  28069  frgrawopreglem2  28148  usg2spot2nb  28168  onfrALTlem5  28339  onfrALTlem1  28345  a9e2nd  28356  2sb5nd  28358  en3lplem2VD  28665  relopabVD  28722  a9e2ndVD  28729  2sb5ndVD  28731  a9e2ndALT  28752  2sb5ndALT  28754  bnj89  28792  bnj133  28798  bnj1019  28856  bnj1101  28861  bnj1109  28863  bnj1143  28867  bnj1198  28873  bnj1304  28897  bnj605  28984  bnj607  28993  bnj600  28996  bnj865  29000  bnj916  29010  bnj983  29028  bnj985  29030  bnj996  29032  bnj1033  29044  bnj1083  29053  bnj1090  29054  bnj1093  29055  bnj1110  29057  bnj1128  29065  bnj1145  29068  bnj1171  29075  bnj1172  29076  bnj1174  29078  bnj1176  29080  bnj1186  29082  bnj1189  29084  bnj1253  29092  bnj1279  29093  bnj1371  29104  bnj1374  29106  bnj1312  29133  equsexNEW7  29196  exsbOLDNEW7  29301  2sb5NEW7  29310  sbel2xNEW7  29315  excom13OLD7  29379  exrot4OLD7  29381  eeorOLD7  29383  19.12vvOLD7  29385  eeanOLD7  29386  eeeanvOLD7  29388  ee4anvOLD7  29389  2sb5rfOLD7  29446  2exsbOLD7  29452  islshpat  29500  islpln5  30017  islvol5  30061  pmapglb  30252  polval2N  30388  cdlemftr3  31047  dibelval3  31630  dicelval3  31663  dihglb2  31825
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563
This theorem depends on definitions:  df-bi 178  df-ex 1548
  Copyright terms: Public domain W3C validator