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

Metamath Proof Explorer

Theorem rspcdva

Description: Restricted specialization, using implicit substitution. (Contributed by Thierry Arnoux, 21-Jun-2020)

Ref Expression
Hypotheses rspcdva.1 ⊢ x = C → ψ ↔ χ
rspcdva.2 ⊢ φ → ∀ x ∈ A ψ
rspcdva.3 ⊢ φ → C ∈ A
Assertion rspcdva ⊢ φ → χ

Proof

Step Hyp Ref Expression
1 rspcdva.1 ⊢ x = C → ψ ↔ χ
2 rspcdva.2 ⊢ φ → ∀ x ∈ A ψ
3 rspcdva.3 ⊢ φ → C ∈ A
4 1 rspcv ⊢ C ∈ A → ∀ x ∈ A ψ → χ
5 3 2 4 sylc ⊢ φ → χ