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	$$⊢Ⅎx\psi$$
	rspcegf.2	$$⊢\underset{\_}{Ⅎ}xA$$
	rspcegf.3	$$⊢\underset{\_}{Ⅎ}xB$$
	rspcegf.4	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	rspcegf	$$⊢\left(A\in B\wedge \psi \right)\to \exists x\in B\phi$$

Proof

Step	Hyp	Ref	Expression
1		rspcegf.1	$$⊢Ⅎx\psi$$
2		rspcegf.2	$$⊢\underset{\_}{Ⅎ}xA$$
3		rspcegf.3	$$⊢\underset{\_}{Ⅎ}xB$$
4		rspcegf.4	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
5	2 3	nfel	$$⊢ℲxA\in B$$
6	5 1	nfan	$$⊢Ⅎx\left(A\in B\wedge \psi \right)$$
7		eleq1	$$⊢x=A\to \left(x\in B\leftrightarrow A\in B\right)$$
8	7 4	anbi12d	$$⊢x=A\to \left(\left(x\in B\wedge \phi \right)\leftrightarrow \left(A\in B\wedge \psi \right)\right)$$
9	2 6 8	spcegf	$$⊢A\in B\to \left(\left(A\in B\wedge \psi \right)\to \exists x\left(x\in B\wedge \phi \right)\right)$$
10	9	anabsi5	$$⊢\left(A\in B\wedge \psi \right)\to \exists x\left(x\in B\wedge \phi \right)$$
11		df-rex	$$⊢\exists x\in B\phi \leftrightarrow \exists x\left(x\in B\wedge \phi \right)$$
12	10 11	sylibr	$$⊢\left(A\in B\wedge \psi \right)\to \exists x\in B\phi$$