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

Theorem exbidv 1848
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 1837 . 2 (𝜑 → ∀𝑥𝜑)
2 albidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2exbidh 1792 1 (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wex 1702
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837
This theorem depends on definitions:  df-bi 197  df-ex 1703
This theorem is referenced by:  2exbidv  1850  3exbidv  1851  eubid  2486  eleq1w  2682  eleq2w  2683  eleq1d  2684  eleq2dALT  2686  rexbidv2  3044  ceqsex2  3239  alexeqg  3326  sbc2or  3438  sbc5  3454  sbcex2  3480  sbcabel  3510  elpreqprlem  4386  elpreqpr  4387  eluni  4430  csbuni  4457  intab  4498  cbvopab1  4714  cbvopab1s  4716  axrep1  4763  axrep2  4764  axrep3  4765  zfrepclf  4768  axsep2  4773  zfauscl  4774  euotd  4965  opeliunxp  5160  brcog  5277  elrn2g  5302  dfdmf  5306  eldmg  5308  dfrnf  5353  elrn2  5354  elrnmpt1  5363  brcodir  5503  dfco2a  5623  cores  5626  sbcfung  5900  brprcneu  6171  ssimaexg  6251  dmfco  6259  fndmdif  6307  fmptco  6382  fliftf  6550  cbvoprab1  6712  cbvoprab2  6713  snnexOLD  6952  uniuni  6956  dmtpos  7349  wrecseq123  7393  wfrlem1  7399  wfrlem3a  7402  wfrlem15  7414  rdglim2  7513  ecdmn0  7774  mapsn  7884  bren  7949  brdomg  7950  domeng  7954  isinf  8158  ac6sfi  8189  ordiso  8406  brwdom  8457  brwdom2  8463  zfregcl  8484  zfregclOLD  8486  inf0  8503  zfinf  8521  bnd2  8741  isinffi  8803  acneq  8851  acni  8853  aceq0  8926  aceq3lem  8928  dfac3  8929  dfac5lem4  8934  dfac8  8942  dfac9  8943  kmlem1  8957  kmlem2  8958  kmlem8  8964  kmlem10  8966  kmlem13  8969  cfval  9054  cardcf  9059  cfeq0  9063  cfsuc  9064  cff1  9065  cflim3  9069  cofsmo  9076  isfin4  9104  axcc2lem  9243  axcc4dom  9248  domtriomlem  9249  dcomex  9254  axdc2lem  9255  axdc4lem  9262  zfac  9267  ac7g  9281  ac4c  9283  ac5  9284  ac6sg  9295  weth  9302  axrepndlem1  9399  axunndlem1  9402  zfcndrep  9421  zfcndinf  9425  zfcndac  9426  gruina  9625  grothomex  9636  genpass  9816  1idpr  9836  ltexprlem3  9845  ltexprlem4  9846  ltexpri  9850  reclem2pr  9855  reclem3pr  9856  recexpr  9858  infm3  10967  nnunb  11273  axdc4uz  12766  ishashinf  13230  relexpindlem  13784  sumeq1  14400  sumeq2w  14403  sumeq2ii  14404  summo  14429  fsum  14432  fsum2dlem  14482  ntrivcvgn0  14611  ntrivcvgmullem  14614  prodeq1f  14619  prodeq2w  14623  prodeq2ii  14624  prodmo  14647  zprod  14648  fprod  14652  fprodntriv  14653  fprod2dlem  14691  ncoprmgcdne1b  15344  vdwapun  15659  vdwmc  15663  vdwmc2  15664  isacs  16293  dfiso2  16413  brssc  16455  isssc  16461  equivestrcsetc  16773  dirge  17218  gsumvalx  17251  gsumpropd  17253  gsumpropd2lem  17254  gsumress  17257  gsumval3eu  18286  gsumval3lem2  18288  dprd2d2  18424  znleval  19884  neitr  20965  cmpcovf  21175  hausmapdom  21284  ptval  21354  elpt  21356  ptpjopn  21396  ptclsg  21399  ptcnp  21406  uffix2  21709  cnextf  21851  prdsxmslem2  22315  metustfbas  22343  metcld2  23086  dchrmusumlema  25163  dchrisum0lema  25184  istrkgld  25339  uvtxa01vtx0  26278  1loopgrvd2  26380  wspthsn  26716  iswspthn  26717  wspthsnon  26720  iswspthsnon  26722  wspthnon  26724  wlkiswwlks2  26742  wlkiswwlksupgr2  26744  wlklnwwlkln2lem  26749  wlksnwwlknvbij  26784  wspthsnwspthsnon  26792  elwwlks2on  26833  elwwlks2  26842  elwspths2spth  26843  clwlkclwwlk  26884  clwwlksvbij  26902  isgrpo  27321  adjeu  28718  fcoinvbr  29391  fmptcof2  29430  acunirnmpt  29432  acunirnmpt2  29433  acunirnmpt2f  29434  aciunf1  29436  fpwrelmapffslem  29481  fmcncfil  29951  bnj865  30967  bnj1388  31075  bnj1489  31098  eldm3  31627  opelco3  31652  frrlem1  31754  elsingles  32000  funpartlem  32024  dfrdg4  32033  linedegen  32225  finminlem  32287  filnetlem4  32351  bj-axrep1  32763  bj-axrep2  32764  bj-axrep3  32765  bj-issetwt  32834  bj-ax8  32862  bj-axsep2  32896  bj-restuni  33025  bj-finsumval0  33118  csbwrecsg  33144  csboprabg  33147  topdifinffinlem  33166  wl-sb8eut  33330  sdclem1  33510  fdc  33512  ismgmOLD  33620  isriscg  33754  islshpat  34123  lshpsmreu  34215  isopos  34286  islpln5  34640  islvol5  34684  pmapjat1  34958  dibelval3  36255  diblsmopel  36279  mapdpglem3  36783  hdmapglem7a  37038  dfac11  37451  clcnvlem  37749  dfhe3  37889  ntrneineine0lem  38201  iotasbc  38440  iotasbc2  38441  sbcexgOLD  38573  csbunigOLD  38871  csbxpgOLD  38873  csbrngOLD  38876  fnchoice  39008  mapsnd  39204  mapsnend  39207  axccdom  39232  axccd  39245  stoweidlem35  40015  stoweidlem39  40019  elsprel  41490  opeliun2xp  41876  bnd2d  42193
  Copyright terms: Public domain W3C validator