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

Theorem rspcedv 3074
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 3072 1  |-  ( ph  ->  ( ch  ->  E. x  e.  B  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1364    e. wcel 1761   E.wrex 2714
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ral 2718  df-rex 2719  df-v 2972
This theorem is referenced by:  0csh0  12426  gcdcllem1  13691  symgmatr01lem  18359  f1otrg  23036  cusgrafilem2  23307  xrofsup  25972  rexzrexnn0  29051  wwlknredwwlkn  30267  usg2cwwkdifex  30404  wwlkextprop  30472  numclwwlkun  30581  numclwlk1lem2fo  30597  scmatid  30748  scmatsubcl  30750  scmatmulcl  30752  lcoel0  30786  lcoss  30794  el0ldep  30824  ldepspr  30831  islindeps2  30841  isldepslvec2  30843
  Copyright terms: Public domain W3C validator