Theorem rspced

Description: Restricted existential specialization, using implicit substitution. (Contributed by Glauco Siliprandi, 15-Feb-2025)

	Ref	Expression
Hypotheses	rspced.1	⊢ Ⅎ 𝑥 𝜒
	rspced.2	⊢ Ⅎ 𝑥 𝐴
	rspced.3	⊢ Ⅎ 𝑥 𝐵
	rspced.4	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
	rspced.5	⊢ ( 𝜑 → 𝜒 )
	rspced.6	⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜒 ) )
Assertion	rspced	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		rspced.1	⊢ Ⅎ 𝑥 𝜒
2		rspced.2	⊢ Ⅎ 𝑥 𝐴
3		rspced.3	⊢ Ⅎ 𝑥 𝐵
4		rspced.4	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
5		rspced.5	⊢ ( 𝜑 → 𝜒 )
6		rspced.6	⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜒 ) )
7	1 2 3 6	rspcef	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝜒 ) → ∃ 𝑥 ∈ 𝐵 𝜓 )
8	4 5 7	syl2anc	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 𝜓 )