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

Theorem exbidv 2012
Description: Formula-building rule for existential quantifier (deduction form). (Contributed by NM, 26-May-1993.)
Hypothesis
Ref Expression
albidv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
exbidv (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem exbidv
StepHypRef Expression
1 ax-5 2001 . 2 (𝜑 → ∀𝑥𝜑)
2 albidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2exbidh 1955 1 (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wex 1859
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001
This theorem depends on definitions:  df-bi 198  df-ex 1860
This theorem is referenced by:  nfbidv  2013  2exbidv  2015  3exbidv  2016  mobidv  2636  eubidv  2647  eubidvOLDOLD  2648  mobidvOLDOLD  2649  eubid  2662  eleq1w  2879  eleq2w  2880  eleq1d  2881  eleq2dALT  2883  rexbidv2  3247  ceqsex2  3449  alexeqg  3537  sbc2or  3653  sbc5  3669  sbcex2  3695  sbcabel  3723  elpreqprlem  4599  elpreqpr  4600  eluni  4644  csbuni  4671  intab  4710  cbvopab1  4928  cbvopab1s  4930  axrep1  4978  axreplem  4979  zfrepclf  4984  axsep2  4989  zfauscl  4990  euotd  5181  opeliunxp  5384  brcog  5504  elrn2g  5528  dfdmf  5532  eldmg  5534  dfrnf  5579  elrn2  5580  elrnmpt1  5589  brcodir  5740  dfco2a  5863  cores  5866  sbcfung  6135  brprcneu  6410  ssimaexg  6495  dmfco  6503  fndmdif  6553  fmptco  6629  fliftf  6799  cbvoprab1  6967  cbvoprab2  6968  snnexOLD  7207  uniuni  7211  dmtpos  7609  wrecseq123  7653  wfrlem1  7659  wfrlem3a  7662  wfrlem15  7675  rdglim2  7774  ecdmn0  8034  mapsnd  8144  bren  8211  brdomg  8212  domeng  8216  mapsnend  8281  isinf  8422  ac6sfi  8453  ordiso  8670  brwdom  8721  brwdom2  8727  zfregcl  8748  inf0  8775  zfinf  8793  bnd2  9013  isinffi  9111  acneq  9159  acni  9161  aceq0  9234  aceq3lem  9236  dfac3  9237  dfac5lem4  9242  dfac8  9252  dfac9  9253  kmlem1  9267  kmlem2  9268  kmlem8  9274  kmlem10  9276  kmlem13  9279  cfval  9364  cardcf  9369  cfeq0  9373  cfsuc  9374  cff1  9375  cflim3  9379  cofsmo  9386  isfin4  9414  axcc2lem  9553  axcc4dom  9558  domtriomlem  9559  dcomex  9564  axdc2lem  9565  axdc4lem  9572  zfac  9577  ac7g  9591  ac4c  9593  ac5  9594  ac6sg  9605  weth  9612  axrepndlem1  9709  axunndlem1  9712  zfcndrep  9731  zfcndinf  9735  zfcndac  9736  gruina  9935  grothomex  9946  genpass  10126  1idpr  10146  ltexprlem3  10155  ltexprlem4  10156  ltexpri  10160  reclem2pr  10165  reclem3pr  10166  recexpr  10168  infm3  11277  nnunb  11575  axdc4uz  13027  ishashinf  13484  relexpindlem  14046  sumeq1  14662  sumeq2w  14665  sumeq2ii  14666  summo  14691  fsum  14694  fsum2dlem  14744  ntrivcvgn0  14871  ntrivcvgmullem  14874  prodeq1f  14879  prodeq2w  14883  prodeq2ii  14884  prodmo  14907  zprod  14908  fprod  14912  fprodntriv  14913  fprod2dlem  14951  ncoprmgcdne1b  15602  vdwapun  15915  vdwmc  15919  vdwmc2  15920  isacs  16536  dfiso2  16656  brssc  16698  isssc  16704  equivestrcsetc  17017  dirge  17462  gsumvalx  17495  gsumpropd  17497  gsumpropd2lem  17498  gsumress  17501  gsumval3eu  18526  gsumval3lem2  18528  dprd2d2  18665  znleval  20130  neitr  21219  cmpcovf  21429  hausmapdom  21538  ptval  21608  elpt  21610  ptpjopn  21650  ptclsg  21653  ptcnp  21660  uffix2  21962  cnextf  22104  prdsxmslem2  22568  metustfbas  22596  metcld2  23339  dchrmusumlema  25419  dchrisum0lema  25440  istrkgld  25595  uvtx01vtx  26541  uvtxa01vtx0OLD  26543  1loopgrvd2  26650  wspthsn  26993  iswspthn  26994  wspthsnon  26997  iswspthsnon  27002  iswspthsnonOLD  27003  wspthnon  27005  wspthnonOLD  27007  wspthnonOLDOLD  27008  wlkiswwlks2  27025  wlkiswwlksupgr2  27027  wlklnwwlkln2lem  27032  wlksnwwlknvbij  27068  wlksnwwlknvbijOLD  27069  wspthsnwspthsnon  27077  wspthsnwspthsnonOLD  27079  elwwlks2on  27123  elwwlks2  27131  elwspths2spth  27132  clwlkclwwlk  27168  clwwlkvbij  27305  clwwlkvbijOLDOLD  27306  clwwlkvbijOLD  27307  isgrpo  27703  adjeu  29099  fcoinvbr  29767  fmptcof2  29807  acunirnmpt  29809  acunirnmpt2  29810  acunirnmpt2f  29811  aciunf1  29813  fpwrelmapffslem  29857  fmcncfil  30325  bnj865  31338  bnj1388  31446  bnj1489  31469  eldm3  31995  opelco3  32020  frecseq123  32120  frrlem1  32123  elsingles  32368  funpartlem  32392  dfrdg4  32401  linedegen  32593  finminlem  32655  filnetlem4  32719  bj-axrep1  33121  bj-axrep2  33122  bj-axrep3  33123  bj-issetwt  33186  bj-ax8  33214  bj-axsep2  33250  bj-restuni  33380  bj-finsumval0  33483  csbwrecsg  33509  csboprabg  33512  topdifinffinlem  33530  wl-sb8eut  33692  sdclem1  33869  fdc  33871  ismgmOLD  33979  isriscg  34113  eldm4  34373  exan3  34398  exanres  34399  eldmcnv  34445  brxrn  34468  cosseq  34513  brcoss  34518  brcoss3  34520  eldm1cossres  34542  brcosscnv  34554  islshpat  34816  lshpsmreu  34908  isopos  34979  islpln5  35334  islvol5  35378  pmapjat1  35652  dibelval3  36946  diblsmopel  36970  mapdpglem3  37474  hdmapglem7a  37726  dfac11  38151  clcnvlem  38448  dfhe3  38587  ntrneineine0lem  38899  iotasbc  39137  iotasbc2  39138  sbcexgOLD  39269  csbxpgOLD  39566  csbrngOLD  39569  fnchoice  39700  axccdom  39921  axccd  39931  stoweidlem35  40749  stoweidlem39  40753  dfatdmfcoafv2  41861  dfatco  41863  elsprel  42311  opeliun2xp  42697  bnd2d  43014
  Copyright terms: Public domain W3C validator