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

Metamath Proof Explorer

Theorem spcv

Description: Rule of specialization, using implicit substitution. (Contributed by NM, 22-Jun-1994)

Ref Expression
Hypotheses spcv.1 ⊢ A ∈ V
spcv.2 ⊢ x = A → φ ↔ ψ
Assertion spcv ⊢ ∀ x φ → ψ

Proof

Step Hyp Ref Expression
1 spcv.1 ⊢ A ∈ V
2 spcv.2 ⊢ x = A → φ ↔ ψ
3 2 spcgv ⊢ A ∈ V → ∀ x φ → ψ
4 1 3 ax-mp ⊢ ∀ x φ → ψ