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 ⊢ Ⅎ x χ
rspced.2 ⊢ Ⅎ _ x A
rspced.3 ⊢ Ⅎ _ x B
rspced.4 ⊢ φ → A ∈ B
rspced.5 ⊢ φ → χ
rspced.6 ⊢ x = A → ψ ↔ χ
Assertion rspced ⊢ φ → ∃ x ∈ B ψ

Proof

Step Hyp Ref Expression
1 rspced.1 ⊢ Ⅎ x χ
2 rspced.2 ⊢ Ⅎ _ x A
3 rspced.3 ⊢ Ⅎ _ x B
4 rspced.4 ⊢ φ → A ∈ B
5 rspced.5 ⊢ φ → χ
6 rspced.6 ⊢ x = A → ψ ↔ χ
7 1 2 3 6 rspcef ⊢ A ∈ B ∧ χ → ∃ x ∈ B ψ
8 4 5 7 syl2anc ⊢ φ → ∃ x ∈ B ψ