Theorem rspcef

Description: Restricted existential specialization, using implicit substitution. (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	rspcef.1	⊢ Ⅎ 𝑥 𝜓
	rspcef.2	⊢ Ⅎ 𝑥 𝐴
	rspcef.3	⊢ Ⅎ 𝑥 𝐵
	rspcef.4	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
Assertion	rspcef	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝜓 ) → ∃ 𝑥 ∈ 𝐵 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		rspcef.1	⊢ Ⅎ 𝑥 𝜓
2		rspcef.2	⊢ Ⅎ 𝑥 𝐴
3		rspcef.3	⊢ Ⅎ 𝑥 𝐵
4		rspcef.4	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
5	1 2 3 4	rspcegf	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝜓 ) → ∃ 𝑥 ∈ 𝐵 𝜑 )