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

Theorem rspcedv 3077
Description: Restricted existential specialization, using implicit substitution. (Contributed by FL, 17-Apr-2007.) (Revised by Mario Carneiro, 4-Jan-2017.)
Hypotheses
Ref Expression
rspcdv.1  |-  ( ph  ->  A  e.  B )
rspcdv.2  |-  ( (
ph  /\  x  =  A )  ->  ( ps 
<->  ch ) )
Assertion
Ref Expression
rspcedv  |-  ( ph  ->  ( ch  ->  E. x  e.  B  ps )
)
Distinct variable groups:    x, A    x, B    ph, x    ch, x
Allowed substitution hint:    ps( x)

Proof of Theorem rspcedv
StepHypRef Expression
1 rspcdv.1 . 2  |-  ( ph  ->  A  e.  B )
2 rspcdv.2 . . 3  |-  ( (
ph  /\  x  =  A )  ->  ( ps 
<->  ch ) )
32biimprd 223 . 2  |-  ( (
ph  /\  x  =  A )  ->  ( ch  ->  ps ) )
41, 3rspcimedv 3075 1  |-  ( ph  ->  ( ch  ->  E. x  e.  B  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1369    e. wcel 1756   E.wrex 2716
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ral 2720  df-rex 2721  df-v 2974
This theorem is referenced by:  0csh0  12430  gcdcllem1  13695  symgmatr01lem  18459  f1otrg  23117  cusgrafilem2  23388  xrofsup  26055  rexzrexnn0  29142  wwlknredwwlkn  30358  usg2cwwkdifex  30495  wwlkextprop  30563  numclwwlkun  30672  numclwlk1lem2fo  30688  ssnn0fi  30746  fsuppmapnn0fiub  30799  fsuppmapnn0fiubex  30800  nn0gsumfz  30804  ply1mulgsumlem1  30844  ply1mulgsumlem2  30845  scmatid  30882  scmatsubcl  30884  scmatmulcl  30886  pmatcoe1fsupp  30892  pmattomply1fo  30923  lcoel0  30962  lcoss  30970  el0ldep  31000  ldepspr  31007  islindeps2  31017  isldepslvec2  31019
  Copyright terms: Public domain W3C validator