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

Theorem rspcedvd 3154
Description: Restricted existential specialization, using implicit substitution. Variant of rspcdv 3152. (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 3153 . 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 188    /\ wa 371    = wceq 1443    e. wcel 1886   E.wrex 2737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ral 2741  df-rex 2742  df-v 3046
This theorem is referenced by:  rspcedeq1vd  3155  rspcedeq2vd  3156  fsnex  6179  negfi  10551  fiminre  10552  reltre  11627  rpltrp  11628  reltxrnmnf  11629  ssnn0fi  12194  fsuppmapnn0fiubex  12201  lcmscllemOLD  14575  fissn0dvds  14582  ncoprmlnprm  14670  prmgaplem2  15001  prmgaplcmlem2  15003  prmgaplcmlem2OLD  15006  prmgapprmorlemOLD  15010  prmgaplem5  15018  prmgapprmolem  15025  fullestrcsetc  16029  equivestrcsetc  16030  fullsetcestrc  16044  isnsgrp  16524  mgmnsgrpex  16658  sgrpnmndex  16659  cply1coe0bi  18887  scmatid  19532  scmataddcl  19534  scmatsubcl  19535  scmatmulcl  19536  scmatrhmcl  19546  mat0scmat  19556  symgmatr01lem  19671  pmatcoe1fsupp  19718  cpmatacl  19733  cpmatinvcl  19734  m2cpmfo  19773  pmatcollpw3fi1lem2  19804  islnoppd  24775  outpasch  24790  hlpasch  24791  colopp  24804  colhp  24805  inaghl  24874  f1otrg  24894  fargshiftfo  25359  usg2cwwkdifex  25542  numclwlk1lem2fo  25816  1stpreimas  28279  gsummpt2d  28537  esum2d  28907  imo72b2lem0  36602  imo72b2lem2  36604  imo72b2lem1  36608  imo72b2  36613  elmod2OLD  38720  iccelpart  38741  dfodd6  38761  dfeven4  38762  opoeALTV  38806  opeoALTV  38807  nn0onn0exALTV  38821  nn0enn0exALTV  38822  bgoldbst  38873  nnsum3primesgbe  38881  nnsum4primesodd  38885  nnsum4primesoddALTV  38886  evengpop3  38887  evengpoap3  38888  nnsum4primeseven  38889  nnsum4primesevenALTV  38890  wtgoldbnnsum4prm  38891  bgoldbnnsum3prm  38893  bgoldbtbndlem4  38897  bgoldbtbnd  38898  bgoldbachlt  38900  tgoldbachlt  38903  41prothprm  38913  clel5  38975  elpr2elpr  38997  usgredg4  39280  nbupgr  39395  nbumgrvtx  39397  nbgr2vtx1edg  39401  nbuhgr2vtx1edgb  39403  nbusgredgeu  39423  cusgrexi  39490  1wlkvtxiedg  39620  usgvincvad  39703  usgvincvadALT  39706  1odd  39798  nnsgrpnmnd  39805  0even  39918  2even  39920  2zlidl  39921  2zrngamgm  39926  2zrngamnd  39928  2zrngagrp  39930  2zrngmmgm  39933  2zrngnmlid  39936  ply1mulgsumlem1  40165  ply1mulgsumlem2  40166  el0ldep  40246  mod0mul  40309  nn0onn0ex  40318  nn0enn0ex  40319  nnpw2p  40384
  Copyright terms: Public domain W3C validator