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

Theorem exbidv 1890
Description: Formula-building rule for existential quantifier (deduction rule). (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 1879 . 2 (𝜑 → ∀𝑥𝜑)
2 albidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2exbidh 1834 1 (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wex 1744
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879
This theorem depends on definitions:  df-bi 197  df-ex 1745
This theorem is referenced by:  2exbidv  1892  3exbidv  1893  eubid  2516  eleq1w  2713  eleq2w  2714  eleq1d  2715  eleq2dALT  2717  rexbidv2  3077  ceqsex2  3275  alexeqg  3363  sbc2or  3477  sbc5  3493  sbcex2  3519  sbcabel  3550  elpreqprlem  4426  elpreqpr  4427  eluni  4471  csbuni  4498  intab  4539  cbvopab1  4756  cbvopab1s  4758  axrep1  4805  axrep2  4806  axrep3  4807  zfrepclf  4810  axsep2  4815  zfauscl  4816  euotd  5004  opeliunxp  5204  brcog  5321  elrn2g  5345  dfdmf  5349  eldmg  5351  dfrnf  5396  elrn2  5397  elrnmpt1  5406  brcodir  5550  dfco2a  5673  cores  5676  sbcfung  5950  brprcneu  6222  ssimaexg  6303  dmfco  6311  fndmdif  6361  fmptco  6436  fliftf  6605  cbvoprab1  6769  cbvoprab2  6770  snnexOLD  7009  uniuni  7013  dmtpos  7409  wrecseq123  7453  wfrlem1  7459  wfrlem3a  7462  wfrlem15  7474  rdglim2  7573  ecdmn0  7832  mapsn  7941  bren  8006  brdomg  8007  domeng  8011  isinf  8214  ac6sfi  8245  ordiso  8462  brwdom  8513  brwdom2  8519  zfregcl  8540  inf0  8556  zfinf  8574  bnd2  8794  isinffi  8856  acneq  8904  acni  8906  aceq0  8979  aceq3lem  8981  dfac3  8982  dfac5lem4  8987  dfac8  8995  dfac9  8996  kmlem1  9010  kmlem2  9011  kmlem8  9017  kmlem10  9019  kmlem13  9022  cfval  9107  cardcf  9112  cfeq0  9116  cfsuc  9117  cff1  9118  cflim3  9122  cofsmo  9129  isfin4  9157  axcc2lem  9296  axcc4dom  9301  domtriomlem  9302  dcomex  9307  axdc2lem  9308  axdc4lem  9315  zfac  9320  ac7g  9334  ac4c  9336  ac5  9337  ac6sg  9348  weth  9355  axrepndlem1  9452  axunndlem1  9455  zfcndrep  9474  zfcndinf  9478  zfcndac  9479  gruina  9678  grothomex  9689  genpass  9869  1idpr  9889  ltexprlem3  9898  ltexprlem4  9899  ltexpri  9903  reclem2pr  9908  reclem3pr  9909  recexpr  9911  infm3  11020  nnunb  11326  axdc4uz  12823  ishashinf  13285  relexpindlem  13847  sumeq1  14463  sumeq2w  14466  sumeq2ii  14467  summo  14492  fsum  14495  fsum2dlem  14545  ntrivcvgn0  14674  ntrivcvgmullem  14677  prodeq1f  14682  prodeq2w  14686  prodeq2ii  14687  prodmo  14710  zprod  14711  fprod  14715  fprodntriv  14716  fprod2dlem  14754  ncoprmgcdne1b  15410  vdwapun  15725  vdwmc  15729  vdwmc2  15730  isacs  16359  dfiso2  16479  brssc  16521  isssc  16527  equivestrcsetc  16839  dirge  17284  gsumvalx  17317  gsumpropd  17319  gsumpropd2lem  17320  gsumress  17323  gsumval3eu  18351  gsumval3lem2  18353  dprd2d2  18489  znleval  19951  neitr  21032  cmpcovf  21242  hausmapdom  21351  ptval  21421  elpt  21423  ptpjopn  21463  ptclsg  21466  ptcnp  21473  uffix2  21775  cnextf  21917  prdsxmslem2  22381  metustfbas  22409  metcld2  23151  dchrmusumlema  25227  dchrisum0lema  25248  istrkgld  25403  uvtx01vtx  26346  uvtxa01vtx0OLD  26348  1loopgrvd2  26455  wspthsn  26797  iswspthn  26798  wspthsnon  26801  iswspthsnon  26806  iswspthsnonOLD  26807  wspthnon  26809  wspthnonOLD  26811  wspthnonOLDOLD  26812  wlkiswwlks2  26829  wlkiswwlksupgr2  26831  wlklnwwlkln2lem  26836  wlksnwwlknvbij  26871  wspthsnwspthsnon  26879  wspthsnwspthsnonOLD  26881  elwwlks2on  26925  elwwlks2  26933  elwspths2spth  26934  clwlkclwwlk  26968  clwwlkvbij  27088  clwwlkvbijOLD  27089  isgrpo  27479  adjeu  28876  fcoinvbr  29545  fmptcof2  29585  acunirnmpt  29587  acunirnmpt2  29588  acunirnmpt2f  29589  aciunf1  29591  fpwrelmapffslem  29635  fmcncfil  30105  bnj865  31119  bnj1388  31227  bnj1489  31250  eldm3  31777  opelco3  31802  frecseq123  31902  frrlem1  31905  elsingles  32150  funpartlem  32174  dfrdg4  32183  linedegen  32375  finminlem  32437  filnetlem4  32501  bj-axrep1  32913  bj-axrep2  32914  bj-axrep3  32915  bj-issetwt  32984  bj-ax8  33012  bj-axsep2  33046  bj-restuni  33175  bj-finsumval0  33277  csbwrecsg  33303  csboprabg  33306  topdifinffinlem  33325  wl-sb8eut  33489  sdclem1  33669  fdc  33671  ismgmOLD  33779  isriscg  33913  eldm4  34178  exan3  34203  exanres  34204  eldmcnv  34253  brxrn  34276  cosseq  34321  brcoss  34326  brcoss3  34328  eldm1cossres  34350  brcosscnv  34362  islshpat  34622  lshpsmreu  34714  isopos  34785  islpln5  35139  islvol5  35183  pmapjat1  35457  dibelval3  36753  diblsmopel  36777  mapdpglem3  37281  hdmapglem7a  37536  dfac11  37949  clcnvlem  38247  dfhe3  38386  ntrneineine0lem  38698  iotasbc  38937  iotasbc2  38938  sbcexgOLD  39070  csbxpgOLD  39368  csbrngOLD  39371  fnchoice  39502  mapsnd  39702  mapsnend  39705  axccdom  39730  axccd  39743  stoweidlem35  40570  stoweidlem39  40574  elsprel  42050  opeliun2xp  42436  bnd2d  42753
  Copyright terms: Public domain W3C validator