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

Theorem exbidv 1714
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:   ,

Proof of Theorem exbidv
StepHypRef Expression
1 ax-5 1704 . 2
2 albidv.1 . 2
31, 2exbidh 1676 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  E.wex 1612
This theorem is referenced by:  2exbidv  1716  3exbidv  1717  eubid  2302  eleq1d  2526  eleq2dALT  2528  eleq1OLD  2531  eleq2OLD  2532  rexbidv2  2964  ceqsex2  3147  alexeqg  3228  alexeq  3229  sbc2or  3336  sbc5  3352  sbcex2  3381  sbcexgOLD  3382  sbcabel  3416  eluni  4252  csbuni  4277  csbunigOLD  4278  intab  4317  cbvopab1  4522  cbvopab1s  4524  axrep1  4564  axrep2  4565  axrep3  4566  zfrepclf  4569  axsep2  4574  zfauscl  4575  euotd  4753  opeliunxp  5056  csbxpgOLD  5087  brcog  5174  elrn2g  5198  dfdmf  5201  eldmg  5203  dfrnf  5246  elrn2  5247  elrnmpt1  5256  brcodir  5391  csbrngOLD  5474  dfco2a  5512  cores  5515  sbcfung  5616  brprcneu  5864  ssimaexg  5939  dmfco  5947  fndmdif  5991  fmptco  6064  fliftf  6213  cbvoprab1  6369  cbvoprab2  6370  snnex  6606  uniuni  6609  dmtpos  6986  rdglim2  7117  ecdmn0  7373  mapsn  7480  bren  7545  brdomg  7546  domeng  7550  isinf  7753  ac6sfi  7784  ordiso  7962  brwdom  8014  brwdom2  8020  zfregcl  8041  inf0  8059  zfinf  8077  bnd2  8332  isinffi  8394  acneq  8445  acni  8447  aceq0  8520  aceq3lem  8522  dfac3  8523  dfac5lem4  8528  dfac8  8536  dfac9  8537  kmlem1  8551  kmlem2  8552  kmlem8  8558  kmlem10  8560  kmlem13  8563  cfval  8648  cardcf  8653  cfeq0  8657  cfsuc  8658  cff1  8659  cflim3  8663  cofsmo  8670  isfin4  8698  axcc2lem  8837  axcc4dom  8842  domtriomlem  8843  dcomex  8848  axdc2lem  8849  axdc4lem  8856  zfac  8861  ac7g  8875  ac4c  8877  ac5  8878  ac6sg  8889  weth  8896  axrepndlem1  8988  axunndlem1  8991  zfcndrep  9013  zfcndinf  9017  zfcndac  9018  gruina  9217  grothomex  9228  genpass  9408  1idpr  9428  ltexprlem3  9437  ltexprlem4  9438  ltexpri  9442  reclem2pr  9447  reclem3pr  9448  recexpr  9450  infm3  10527  nnunb  10816  axdc4uz  12093  sumeq1  13511  sumeq2w  13514  sumeq2ii  13515  summo  13539  fsum  13542  fsum2dlem  13585  ntrivcvgn0  13707  ntrivcvgmullem  13710  prodeq1f  13715  prodeq2w  13719  prodeq2ii  13720  prodmo  13743  zprod  13744  fprod  13748  fprodntriv  13749  fprod2dlem  13784  vdwapun  14492  vdwmc  14496  vdwmc2  14497  isacs  15048  brssc  15183  isssc  15189  dirge  15867  gsumvalx  15897  gsumpropd  15899  gsumpropd2lem  15900  gsumress  15903  gsumval3eu  16907  gsumval3OLD  16908  gsumval3lem2  16910  dprd2d2  17093  znleval  18593  neitr  19681  cmpcovf  19891  hausmapdom  20001  ptval  20071  elpt  20073  ptpjopn  20113  ptclsg  20116  ptcnp  20123  uffix2  20425  cnextf  20566  prdsxmslem2  21032  metustfbasOLD  21068  metustfbas  21069  metcld2  21745  dchrmusumlema  23678  dchrisum0lema  23699  istrkgld  23857  uvtx01vtx  24492  wlkiswwlk2  24697  wlklniswwlkn2  24700  wlknwwlknvbij  24740  clwlkisclwwlk  24789  clwwlkvbij  24801  isgrpo  25198  ismgmOLD  25322  adjeu  26808  fcoinvbr  27461  fmptcof2  27502  fpwrelmapffslem  27555  ishashinf  27606  fmcncfil  27913  relexpindlem  29062  eldm3  29191  opelco3  29208  wrecseq123  29337  wfrlem1  29343  wfrlem15  29357  frrlem1  29387  elsingles  29568  funpartlem  29592  dfrdg4  29600  linedegen  29793  wl-sb8eut  30022  finminlem  30136  filnetlem4  30199  sdclem1  30236  fdc  30238  isriscg  30387  dfac11  31008  iotasbc  31326  iotasbc2  31327  fnchoice  31404  stoweidlem35  31817  stoweidlem39  31821  dfiso2  32568  equivestrcsetc  32658  opeliun2xp  32922  bnj865  33981  bnj1388  34089  bnj1489  34112  bj-axrep1  34374  bj-axrep2  34375  bj-axrep3  34376  bj-eleq1w  34422  bj-eleq2w  34423  bj-issetwt  34435  bj-axsep2  34493  bj-finsumval0  34663  islshpat  34742  lshpsmreu  34834  isopos  34905  islpln5  35259  islvol5  35303  pmapjat1  35577  dibelval3  36874  diblsmopel  36898  mapdpglem3  37402  hdmapglem7a  37657  dfhe3  37799
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704
This theorem depends on definitions:  df-bi 185  df-ex 1613
  Copyright terms: Public domain W3C validator