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

Theorem rspcedv 3164
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 3162 1  |-  ( ph  ->  ( ch  ->  E. x  e.  B  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367    = wceq 1405    e. wcel 1842   E.wrex 2755
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ral 2759  df-rex 2760  df-v 3061
This theorem is referenced by:  rspcedvd  3165  fsuppmapnn0fiub  12141  0csh0  12820  gcdcllem1  14358  nn0gsumfz  17332  pmatcollpw3lem  19576  pmatcollpw3fi1lem2  19580  pm2mpfo  19607  f1otrg  24591  cusgrafilem2  24897  wwlknredwwlkn  25143  wwlkextprop  25161  numclwwlkun  25496  xrofsup  28030  esum2d  28540  rexzrexnn0  35099  ov2ssiunov2  35679  lcoel0  38540  lcoss  38548  el0ldep  38578  ldepspr  38585  islindeps2  38595  isldepslvec2  38597
  Copyright terms: Public domain W3C validator