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	⊢ Ⅎ 𝑥 𝜓
	rspcegf.2	⊢ Ⅎ 𝑥 𝐴
	rspcegf.3	⊢ Ⅎ 𝑥 𝐵
	rspcegf.4	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
Assertion	rspcegf	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝜓 ) → ∃ 𝑥 ∈ 𝐵 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		rspcegf.1	⊢ Ⅎ 𝑥 𝜓
2		rspcegf.2	⊢ Ⅎ 𝑥 𝐴
3		rspcegf.3	⊢ Ⅎ 𝑥 𝐵
4		rspcegf.4	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
5	2 3	nfel	⊢ Ⅎ 𝑥 𝐴 ∈ 𝐵
6	5 1	nfan	⊢ Ⅎ 𝑥 ( 𝐴 ∈ 𝐵 ∧ 𝜓 )
7		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵 ) )
8	7 4	anbi12d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ↔ ( 𝐴 ∈ 𝐵 ∧ 𝜓 ) ) )
9	2 6 8	spcegf	⊢ ( 𝐴 ∈ 𝐵 → ( ( 𝐴 ∈ 𝐵 ∧ 𝜓 ) → ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) )
10	9	anabsi5	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝜓 ) → ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) )
11		df-rex	⊢ ( ∃ 𝑥 ∈ 𝐵 𝜑 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) )
12	10 11	sylibr	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝜓 ) → ∃ 𝑥 ∈ 𝐵 𝜑 )