Theorem rspcedvd 2882

Description: Restricted existential specialization, using implicit substitution. Variant of rspcedv 2880. (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 2880	. 2 |- ( ph -> ( ch -> E. x e. B ps ) )
5	1, 4	mpd 13	1 |- ( ph -> E. x e. B ps )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1372   e. wcel 2175   E.wrex 2484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-rex 2489  df-v 2773

This theorem is referenced by:  rspcime  2883  rspcedeq1vd  2885  rspcedeq2vd  2886  updjud  7183  elpq  9769  modqmuladd  10509  modqmuladdnn0  10511  modfzo0difsn  10538  wrdl1exs1  11081  negfi  11510  divconjdvds  12131  2tp1odd  12166  dfgcd2  12306  qredeu  12390  pw2dvdslemn  12458  dvdsprmpweq  12629  oddprmdvds  12648  gsumfzval  13194  gsumval2  13200  isnsgrp  13209  dfgrp2  13330  grplrinv  13360  grpidinv  13362  dfgrp3m  13402  ringid  13759  xmettx  14953  gausslemma2dlem1a  15506  2lgslem1b  15537  bj-charfunbi  15709