Theorem spcgvOLD

Description: Obsolete version of spcgv as of 25-Aug-2023. (Contributed by NM, 22-Jun-1994) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	spcgv.1	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
Assertion	spcgvOLD	⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 𝜑 → 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		spcgv.1	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
2		nfcv	⊢ Ⅎ 𝑥 𝐴
3		nfv	⊢ Ⅎ 𝑥 𝜓
4	2 3 1	spcgf	⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 𝜑 → 𝜓 ) )