Theorem rspce

Description: Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998) (Revised by Mario Carneiro, 11-Oct-2016)

	Ref	Expression
Hypotheses	rspc.1	|- F/ x ps
	rspc.2	|- ( x = A -> ( ph <-> ps ) )
Assertion	rspce	|- ( ( A e. B /\ ps ) -> E. x e. B ph )

Proof

Step	Hyp	Ref	Expression
1		rspc.1	|- F/ x ps
2		rspc.2	|- ( x = A -> ( ph <-> ps ) )
3		nfcv	|- F/_ x A
4		nfv	|- F/ x A e. B
5	4 1	nfan	|- F/ x ( A e. B /\ ps )
6		eleq1	|- ( x = A -> ( x e. B <-> A e. B ) )
7	6 2	anbi12d	|- ( x = A -> ( ( x e. B /\ ph ) <-> ( A e. B /\ ps ) ) )
8	3 5 7	spcegf	|- ( A e. B -> ( ( A e. B /\ ps ) -> E. x ( x e. B /\ ph ) ) )
9	8	anabsi5	|- ( ( A e. B /\ ps ) -> E. x ( x e. B /\ ph ) )
10		df-rex	|- ( E. x e. B ph <-> E. x ( x e. B /\ ph ) )
11	9 10	sylibr	|- ( ( A e. B /\ ps ) -> E. x e. B ph )