This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝜓 ) → ∃ 𝑥 ∈ 𝐵 𝜑 )