Metamath Proof Explorer


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 x = A φ ψ
Assertion spcgvOLD A V x φ ψ

Proof

Step Hyp Ref Expression
1 spcgv.1 x = A φ ψ
2 nfcv _ x A
3 nfv x ψ
4 2 3 1 spcgf A V x φ ψ