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	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
Assertion	spcgv	⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 𝜑 → 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		spcgv.1	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
2		elex	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
3		elex	⊢ ( 𝐴 ∈ V → 𝐴 ∈ V )
4	1	adantl	⊢ ( ( 𝐴 ∈ V ∧ 𝑥 = 𝐴 ) → ( 𝜑 ↔ 𝜓 ) )
5	3 4	spcdv	⊢ ( 𝐴 ∈ V → ( ∀ 𝑥 𝜑 → 𝜓 ) )
6	2 5	syl	⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 𝜑 → 𝜓 ) )