Metamath Proof Explorer


Theorem vtoclf

Description: Implicit substitution of a class for a setvar variable. This is a generalization of chvar . (Contributed by NM, 30-Aug-1993)

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

Proof

Step Hyp Ref Expression
1 vtoclf.1 x ψ
2 vtoclf.2 A V
3 vtoclf.3 x = A φ ψ
4 vtoclf.4 φ
5 2 isseti x x = A
6 3 biimpd x = A φ ψ
7 5 6 eximii x φ ψ
8 1 7 19.36i x φ ψ
9 8 4 mpg ψ