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

Theorem exbidv 2002
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 1991 . 2 (𝜑 → ∀𝑥𝜑)
2 albidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2exbidh 1945 1 (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wex 1852
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991
This theorem depends on definitions:  df-bi 197  df-ex 1853
This theorem is referenced by:  2exbidv  2004  3exbidv  2005  eubid  2636  eleq1w  2833  eleq2w  2834  eleq1d  2835  eleq2dALT  2837  rexbidv2  3196  ceqsex2  3396  alexeqg  3482  sbc2or  3596  sbc5  3612  sbcex2  3638  sbcabel  3666  elpreqprlem  4532  elpreqpr  4533  eluni  4577  csbuni  4602  intab  4641  cbvopab1  4857  cbvopab1s  4859  axrep1  4905  axreplem  4906  zfrepclf  4911  axsep2  4916  zfauscl  4917  euotd  5106  opeliunxp  5310  brcog  5427  elrn2g  5451  dfdmf  5455  eldmg  5457  dfrnf  5502  elrn2  5503  elrnmpt1  5512  brcodir  5656  dfco2a  5779  cores  5782  sbcfung  6055  brprcneu  6325  ssimaexg  6406  dmfco  6414  fndmdif  6464  fmptco  6539  fliftf  6708  cbvoprab1  6874  cbvoprab2  6875  snnexOLD  7114  uniuni  7118  dmtpos  7516  wrecseq123  7560  wfrlem1  7566  wfrlem3a  7569  wfrlem15  7582  rdglim2  7681  ecdmn0  7941  mapsnd  8051  bren  8118  brdomg  8119  domeng  8123  mapsnend  8188  isinf  8329  ac6sfi  8360  ordiso  8577  brwdom  8628  brwdom2  8634  zfregcl  8655  inf0  8682  zfinf  8700  bnd2  8920  isinffi  9018  acneq  9066  acni  9068  aceq0  9141  aceq3lem  9143  dfac3  9144  dfac5lem4  9149  dfac8  9159  dfac9  9160  kmlem1  9174  kmlem2  9175  kmlem8  9181  kmlem10  9183  kmlem13  9186  cfval  9271  cardcf  9276  cfeq0  9280  cfsuc  9281  cff1  9282  cflim3  9286  cofsmo  9293  isfin4  9321  axcc2lem  9460  axcc4dom  9465  domtriomlem  9466  dcomex  9471  axdc2lem  9472  axdc4lem  9479  zfac  9484  ac7g  9498  ac4c  9500  ac5  9501  ac6sg  9512  weth  9519  axrepndlem1  9616  axunndlem1  9619  zfcndrep  9638  zfcndinf  9642  zfcndac  9643  gruina  9842  grothomex  9853  genpass  10033  1idpr  10053  ltexprlem3  10062  ltexprlem4  10063  ltexpri  10067  reclem2pr  10072  reclem3pr  10073  recexpr  10075  infm3  11184  nnunb  11490  axdc4uz  12991  ishashinf  13449  relexpindlem  14011  sumeq1  14627  sumeq2w  14630  sumeq2ii  14631  summo  14656  fsum  14659  fsum2dlem  14709  ntrivcvgn0  14837  ntrivcvgmullem  14840  prodeq1f  14845  prodeq2w  14849  prodeq2ii  14850  prodmo  14873  zprod  14874  fprod  14878  fprodntriv  14879  fprod2dlem  14917  ncoprmgcdne1b  15571  vdwapun  15885  vdwmc  15889  vdwmc2  15890  isacs  16519  dfiso2  16639  brssc  16681  isssc  16687  equivestrcsetc  17000  dirge  17445  gsumvalx  17478  gsumpropd  17480  gsumpropd2lem  17481  gsumress  17484  gsumval3eu  18512  gsumval3lem2  18514  dprd2d2  18651  znleval  20118  neitr  21205  cmpcovf  21415  hausmapdom  21524  ptval  21594  elpt  21596  ptpjopn  21636  ptclsg  21639  ptcnp  21646  uffix2  21948  cnextf  22090  prdsxmslem2  22554  metustfbas  22582  metcld2  23324  dchrmusumlema  25403  dchrisum0lema  25424  istrkgld  25579  uvtx01vtx  26525  uvtxa01vtx0OLD  26527  1loopgrvd2  26634  wspthsn  26977  iswspthn  26978  wspthsnon  26981  iswspthsnon  26986  iswspthsnonOLD  26987  wspthnon  26989  wspthnonOLD  26991  wspthnonOLDOLD  26992  wlkiswwlks2  27009  wlkiswwlksupgr2  27011  wlklnwwlkln2lem  27016  wlksnwwlknvbij  27052  wlksnwwlknvbijOLD  27053  wspthsnwspthsnon  27061  wspthsnwspthsnonOLD  27063  elwwlks2on  27107  elwwlks2  27115  elwspths2spth  27116  clwlkclwwlk  27152  clwwlkvbij  27289  clwwlkvbijOLDOLD  27290  clwwlkvbijOLD  27291  isgrpo  27691  adjeu  29088  fcoinvbr  29757  fmptcof2  29797  acunirnmpt  29799  acunirnmpt2  29800  acunirnmpt2f  29801  aciunf1  29803  fpwrelmapffslem  29847  fmcncfil  30317  bnj865  31331  bnj1388  31439  bnj1489  31462  eldm3  31989  opelco3  32014  frecseq123  32114  frrlem1  32117  elsingles  32362  funpartlem  32386  dfrdg4  32395  linedegen  32587  finminlem  32649  filnetlem4  32713  bj-axrep1  33124  bj-axrep2  33125  bj-axrep3  33126  bj-issetwt  33188  bj-ax8  33216  bj-axsep2  33252  bj-restuni  33382  bj-finsumval0  33484  csbwrecsg  33510  csboprabg  33513  topdifinffinlem  33532  wl-sb8eut  33693  sdclem1  33871  fdc  33873  ismgmOLD  33981  isriscg  34115  eldm4  34380  exan3  34405  exanres  34406  eldmcnv  34455  brxrn  34478  cosseq  34523  brcoss  34528  brcoss3  34530  eldm1cossres  34552  brcosscnv  34564  islshpat  34826  lshpsmreu  34918  isopos  34989  islpln5  35343  islvol5  35387  pmapjat1  35661  dibelval3  36957  diblsmopel  36981  mapdpglem3  37485  hdmapglem7a  37737  dfac11  38158  clcnvlem  38456  dfhe3  38595  ntrneineine0lem  38907  iotasbc  39146  iotasbc2  39147  sbcexgOLD  39278  csbxpgOLD  39576  csbrngOLD  39579  fnchoice  39710  axccdom  39934  axccd  39947  stoweidlem35  40769  stoweidlem39  40773  elsprel  42253  opeliun2xp  42639  bnd2d  42956
  Copyright terms: Public domain W3C validator