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 ⊢ ( 𝑥 = 𝐶 → ( 𝜓 ↔ 𝜒 ) )
rspcdva.2 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝜓 )
rspcdva.3 ⊢ ( 𝜑 → 𝐶 ∈ 𝐴 )
Assertion rspcdva ( 𝜑 → 𝜒 )

Proof

Step Hyp Ref Expression
1 rspcdva.1 ⊢ ( 𝑥 = 𝐶 → ( 𝜓 ↔ 𝜒 ) )
2 rspcdva.2 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝜓 )
3 rspcdva.3 ⊢ ( 𝜑 → 𝐶 ∈ 𝐴 )
4 1 rspcv ⊢ ( 𝐶 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 𝜓 → 𝜒 ) )
5 3 2 4 sylc ⊢ ( 𝜑 → 𝜒 )