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

Theorem rspcedvd 3140
Description: Restricted existential specialization, using implicit substitution. Variant of rspcdv 3138. (Contributed by AV, 27-Nov-2019.)
Hypotheses
Ref Expression
rspcedvd.1  |-  ( ph  ->  A  e.  B )
rspcedvd.2  |-  ( (
ph  /\  x  =  A )  ->  ( ps 
<->  ch ) )
rspcedvd.3  |-  ( ph  ->  ch )
Assertion
Ref Expression
rspcedvd  |-  ( ph  ->  E. x  e.  B  ps )
Distinct variable groups:    x, A    x, B    ph, x    ch, x
Allowed substitution hint:    ps( x)

Proof of Theorem rspcedvd
StepHypRef Expression
1 rspcedvd.3 . 2  |-  ( ph  ->  ch )
2 rspcedvd.1 . . 3  |-  ( ph  ->  A  e.  B )
3 rspcedvd.2 . . 3  |-  ( (
ph  /\  x  =  A )  ->  ( ps 
<->  ch ) )
42, 3rspcedv 3139 . 2  |-  ( ph  ->  ( ch  ->  E. x  e.  B  ps )
)
51, 4mpd 15 1  |-  ( ph  ->  E. x  e.  B  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367    = wceq 1399    e. wcel 1826   E.wrex 2733
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ral 2737  df-rex 2738  df-v 3036
This theorem is referenced by:  rspcedeq1vd  3141  rspcedeq2vd  3142  ssnn0fi  11997  fsuppmapnn0fiubex  12001  fullestrcsetc  15537  equivestrcsetc  15538  fullsetcestrc  15552  isnsgrp  16032  mgmnsgrpex  16166  sgrpnmndex  16167  cply1coe0bi  18455  scmatid  19101  scmataddcl  19103  scmatsubcl  19104  scmatmulcl  19105  scmatrhmcl  19115  mat0scmat  19125  symgmatr01lem  19240  pmatcoe1fsupp  19287  cpmatacl  19302  cpmatinvcl  19303  m2cpmfo  19342  pmatcollpw3fi1lem2  19373  f1otrg  24295  fargshiftfo  24759  usg2cwwkdifex  24942  numclwlk1lem2fo  25216  1stpreimas  27671  gsummpt2d  27925  esum2d  28241  elmod2OLD  32463  dfodd6  32480  dfeven4  32481  opoeALTV  32525  opeoALTV  32526  nn0onn0exALTV  32540  nn0enn0exALTV  32541  41prothprm  32553  usgvincvad  32722  usgvincvadALT  32725  1odd  32817  nnsgrpnmnd  32824  0even  32937  2even  32939  2zlidl  32940  2zrngamgm  32945  2zrngamnd  32947  2zrngagrp  32949  2zrngmmgm  32952  2zrngnmlid  32955  ply1mulgsumlem1  33186  ply1mulgsumlem2  33187  el0ldep  33267  mod0mul  33332  nn0onn0ex  33341  nn0enn0ex  33342  nnpw2p  33407  imo72b2lem0  38511  imo72b2lem2  38513  imo72b2lem1  38517  imo72b2  38522
  Copyright terms: Public domain W3C validator