Theorem rspcegf

Description: A version of rspcev using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017)

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

Proof

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