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

Metamath Proof Explorer

Theorem rspcimedv

Description: Restricted existential specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses rspcimdv.1 ⊢ φ → A ∈ B
rspcimedv.2 ⊢ φ ∧ x = A → χ → ψ
Assertion rspcimedv ⊢ φ → χ → ∃ x ∈ B ψ

Proof

Step Hyp Ref Expression
1 rspcimdv.1 ⊢ φ → A ∈ B
2 rspcimedv.2 ⊢ φ ∧ x = A → χ → ψ
3 2 con3d ⊢ φ ∧ x = A → ¬ ψ → ¬ χ
4 1 3 rspcimdv ⊢ φ → ∀ x ∈ B ¬ ψ → ¬ χ
5 4 con2d ⊢ φ → χ → ¬ ∀ x ∈ B ¬ ψ
6 dfrex2 ⊢ ∃ x ∈ B ψ ↔ ¬ ∀ x ∈ B ¬ ψ
7 5 6 imbitrrdi ⊢ φ → χ → ∃ x ∈ B ψ