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

Theorem exbidv 1612
Description: Formula-building rule for existential quantifier (deduction rule). (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
albidv.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
exbidv  |-  ( ph  ->  ( E. x ps  <->  E. x ch ) )
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)

Proof of Theorem exbidv
StepHypRef Expression
1 ax-17 1603 . 2  |-  ( ph  ->  A. x ph )
2 albidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2exbidh 1578 1  |-  ( ph  ->  ( E. x ps  <->  E. x ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   E.wex 1528
This theorem is referenced by:  2exbidv  1614  3exbidv  1615  eubid  2150  eleq1  2343  eleq2  2344  rexbidv2  2566  ceqsex2  2824  alexeq  2897  ceqex  2898  sbc2or  2999  sbc5  3015  sbcex2  3040  sbcexg  3041  sbcabel  3068  eluni  3830  csbunig  3835  intab  3892  cbvopab1  4089  cbvopab1s  4091  axrep1  4132  axrep2  4133  axrep3  4134  zfrepclf  4137  axsep2  4142  zfauscl  4143  euotd  4267  snnex  4524  uniuni  4527  csbxpg  4716  opeliunxp  4740  brcog  4850  elrn2g  4870  dfdmf  4873  eldmg  4874  dfrnf  4917  elrn2  4918  csbrng  4923  elrnmpt1  4928  brcodir  5062  dfco2a  5173  cores  5176  brprcneu  5518  ssimaexg  5585  dmfco  5593  fndmdif  5629  fmptco  5691  fliftf  5814  cbvoprab1  5918  cbvoprab2  5919  dmtpos  6246  rdglim2  6445  ecdmn0  6702  mapsn  6809  bren  6871  brdomg  6872  domeng  6876  isinf  7076  ac6sfi  7101  ordiso  7231  brwdom  7281  brwdom2  7287  zfregcl  7308  inf0  7322  zfinf  7340  bnd2  7563  isinffi  7625  acneq  7670  acni  7672  aceq0  7745  aceq3lem  7747  dfac3  7748  dfac5lem4  7753  dfac8  7761  dfac9  7762  kmlem1  7776  kmlem2  7777  kmlem8  7783  kmlem10  7785  kmlem13  7788  cfval  7873  cardcf  7878  cfeq0  7882  cfsuc  7883  cff1  7884  cflim3  7888  cofsmo  7895  isfin4  7923  axcc2lem  8062  axcc4dom  8067  domtriomlem  8068  dcomex  8073  axdc2lem  8074  axdc4lem  8081  zfac  8086  ac7g  8101  ac4c  8103  ac5  8104  ac6sg  8115  weth  8122  axrepndlem1  8214  axunndlem1  8217  zfcndrep  8236  zfcndinf  8240  zfcndac  8241  gruina  8440  grothomex  8451  genpass  8633  1idpr  8653  ltexprlem3  8662  ltexprlem4  8663  ltexpri  8667  reclem2pr  8672  reclem3pr  8673  recexpr  8675  infm3  9713  nnunb  9961  axdc4uz  11045  sumeq1f  12161  sumeq2w  12165  sumeq2ii  12166  cbvsum  12168  summo  12190  fsum  12193  fsum2dlem  12233  vdwapun  13021  vdwmc  13025  vdwmc2  13026  isacs  13553  brssc  13691  isssc  13697  dirge  14359  gsumvalx  14451  gsumpropd  14453  gsumress  14454  gsumval3eu  15190  gsumval3  15191  dprd2d2  15279  znleval  16508  cmpcovf  17118  hausmapdom  17226  ptval  17265  elpt  17267  ptpjopn  17306  ptclsg  17309  ptcnp  17316  uffix2  17619  prdsxmslem2  18075  metcld2  18732  dchrmusumlema  20642  dchrisum0lema  20663  isgrpo  20863  ismgm  20987  adjeu  22469  relexpindlem  23447  eldm3  23530  wfrlem1  23667  wfrlem15  23681  frrlem1  23692  elsingles  23868  brimg  23887  dfrdg4  23899  linedegen  24177  bpolylem  24194  bpolyval  24195  alexeqd  24374  copsexgb  24378  ac5g  24487  surjsec2  24532  islatalg  24595  prodeq1  24718  prodeq2  24719  prodeq3ii  24720  fisub  24966  finminlem  25643  filnetlem4  25742  sdclem1  25865  fdc  25867  isriscg  26027  dfac11  26572  iotasbc  27031  iotasbc2  27032  fnchoice  27112  stoweidlem35  27196  stoweidlem39  27200  csbdmg  27392  sbcfun  27397  bnj865  28328  bnj1388  28436  bnj1489  28459  islshpat  28580  lshpsmreu  28672  isopos  28743  islpln5  29097  islvol5  29141  pmapjat1  29415  dibelval3  30710  diblsmopel  30734  mapdpglem3  31238  hdmapglem7a  31493
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603
This theorem depends on definitions:  df-bi 177  df-ex 1529
  Copyright terms: Public domain W3C validator