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

Proof

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