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

Metamath Proof Explorer

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