Metamath Proof Explorer


Theorem vtoclALT

Description: Alternate proof of vtocl . Shorter but requires more axioms. (Contributed by NM, 30-Aug-1993) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses vtoclALT.1 A V
vtoclALT.2 x = A φ ψ
vtoclALT.3 φ
Assertion vtoclALT ψ

Proof

Step Hyp Ref Expression
1 vtoclALT.1 A V
2 vtoclALT.2 x = A φ ψ
3 vtoclALT.3 φ
4 nfv x ψ
5 4 1 2 3 vtoclf ψ