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

Metamath Proof Explorer

Theorem spcgv

Description: Rule of specialization, using implicit substitution. Compare Theorem 7.3 of Quine p. 44. (Contributed by NM, 22-Jun-1994) Avoid ax-10 , ax-11 . (Revised by Wolf Lammen, 25-Aug-2023)

Ref Expression
Hypothesis spcgv.1 ⊢ x = A → φ ↔ ψ
Assertion spcgv ⊢ A ∈ V → ∀ x φ → ψ

Proof

Step Hyp Ref Expression
1 spcgv.1 ⊢ x = A → φ ↔ ψ
2 elex ⊢ A ∈ V → A ∈ V
3 id ⊢ A ∈ V → A ∈ V
4 1 adantl ⊢ A ∈ V ∧ x = A → φ ↔ ψ
5 3 4 spcdv ⊢ A ∈ V → ∀ x φ → ψ
6 2 5 syl ⊢ A ∈ V → ∀ x φ → ψ