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

Theorem rspcedv 3211
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 3209 1  |-  ( ph  ->  ( ch  ->  E. x  e.  B  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1374    e. wcel 1762   E.wrex 2808
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 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ral 2812  df-rex 2813  df-v 3108
This theorem is referenced by:  rspcedvd  3212  ssnn0fi  12050  fsuppmapnn0fiub  12053  fsuppmapnn0fiubex  12054  0csh0  12714  gcdcllem1  13997  nn0gsumfz  16796  cply1coe0bi  18106  symgmatr01lem  18915  pmatcollpw3lem  19044  pmatcollpw3fi1lem2  19048  pm2mpfo  19075  f1otrg  23843  cusgrafilem2  24142  wwlknredwwlkn  24388  wwlkextprop  24406  numclwwlkun  24742  numclwlk1lem2fo  24758  xrofsup  27236  rexzrexnn0  30328  ply1mulgsumlem1  31934  ply1mulgsumlem2  31935  lcoel0  31977  lcoss  31985  el0ldep  32015  ldepspr  32022  islindeps2  32032  isldepslvec2  32034
  Copyright terms: Public domain W3C validator