Theorem rspcedvd 3317

Description: Restricted existential specialization, using implicit substitution. Variant of rspcedv 3313. (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

Step	Hyp	Ref	Expression
1		rspcedvd.3	. 2 |- ( ph -> ch )
2		rspcedvd.1	. . 3 |- ( ph -> A e. B )
3		rspcedvd.2	. . 3 |- ( ( ph /\ x = A ) -> ( ps <-> ch ) )
4	2, 3	rspcedv 3313	. 2 |- ( ph -> ( ch -> E. x e. B ps ) )
5	1, 4	mpd 15	1 |- ( ph -> E. x e. B ps )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   E.wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-v 3202

This theorem is referenced by:  rspcedeq1vd  3318  rspcedeq2vd  3319  clel5  3343  elpr2elpr  4398  prproe  4434  fsnex  6538  negfi  10971  fiminre  10972  reltre  12170  rpltrp  12171  reltxrnmnf  12172  modmuladd  12712  modmuladdnn0  12714  modfzo0difsn  12742  ssnn0fi  12784  fsuppmapnn0fiubex  12792  cshimadifsn0  13576  divconjdvds  15037  2tp1odd  15076  dfgcd2  15263  fissn0dvds  15332  ncoprmlnprm  15436  dvdsprmpweq  15588  oddprmdvds  15607  prmgaplem2  15754  prmgaplcmlem2  15756  prmgaplem5  15759  prmgapprmolem  15765  fullestrcsetc  16791  equivestrcsetc  16792  fullsetcestrc  16806  isnsgrp  17288  mgmnsgrpex  17418  sgrpnmndex  17419  dfgrp2  17447  grplrinv  17473  grpidinv  17475  dfgrp3  17514  ringid  18574  cply1coe0bi  19670  scmatid  20320  scmataddcl  20322  scmatsubcl  20323  scmatmulcl  20324  scmatrhmcl  20334  mat0scmat  20344  symgmatr01lem  20459  cpmatacl  20521  cpmatinvcl  20522  m2cpmfo  20561  pmatcollpw3fi1lem2  20592  gausslemma2dlem1a  25090  2lgslem1b  25117  islnoppd  25632  outpasch  25647  hlpasch  25648  colopp  25661  colhp  25662  inaghl  25731  f1otrg  25751  usgredg4  26109  nbupgr  26240  nbumgrvtx  26242  nbgr2vtx1edg  26246  nbuhgr2vtx1edgb  26248  nbusgredgeu  26268  cusgrexilem2  26338  wlkvtxiedg  26520  wlkres  26567  elwwlks2ons3  26848  umgr2cwwkdifex  26942  1pthon2ve  27014  numclwlk1lem2fo  27228  1stpreimas  29483  gsummpt2d  29781  esum2d  30155  reprsuc  30693  reprpmtf1o  30704  unblimceq0lem  32497  unblimceq0  32498  unbdqndv2  32502  knoppndvlem19  32521  clsk3nimkb  38338  clsk1indlem1  38343  ntrclsiso  38365  ntrclsk2  38366  ntrclskb  38367  ntrclsk3  38368  ntrclsk13  38369  ntrclsk4  38370  imo72b2lem0  38465  imo72b2lem2  38467  imo72b2lem1  38471  imo72b2  38475  iccelpart  41369  fargshiftfo  41378  fmtnoodd  41445  fmtnoprmfac2lem1  41478  fmtnofac2lem  41480  fmtnofac2  41481  fmtnofac1  41482  41prothprm  41536  dfodd6  41550  dfeven4  41551  opoeALTV  41594  opeoALTV  41595  nn0onn0exALTV  41609  nn0enn0exALTV  41610  mogoldbblem  41629  sbgoldbst  41666  sgoldbeven3prm  41671  sbgoldbo  41675  nnsum3primesgbe  41680  nnsum4primesodd  41684  nnsum4primesoddALTV  41685  evengpop3  41686  evengpoap3  41687  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  wtgoldbnnsum4prm  41690  bgoldbnnsum3prm  41692  bgoldbtbndlem4  41696  bgoldbtbnd  41697  bgoldbachlt  41701  tgoldbachlt  41704  bgoldbachltOLD  41707  tgoldbachltOLD  41710  sprsymrelf1lem  41741  sprsymrelfo  41747  uspgrsprfo  41756  1odd  41811  nnsgrpnmnd  41818  0even  41931  2even  41933  2zlidl  41934  2zrngamgm  41939  2zrngamnd  41941  2zrngagrp  41943  2zrngmmgm  41946  2zrngnmlid  41949  ply1mulgsumlem1  42174  ply1mulgsumlem2  42175  el0ldep  42255  mod0mul  42314  nn0onn0ex  42318  nn0enn0ex  42319  nnpw2p  42380