Metamath Proof Explorer


Theorem vtocl2

Description: Implicit substitution of classes for setvar variables. (Contributed by NM, 26-Jul-1995) (Proof shortened by Andrew Salmon, 8-Jun-2011)

Ref Expression
Hypotheses vtocl2.1 AV
vtocl2.2 BV
vtocl2.3 x=Ay=Bφψ
vtocl2.4 φ
Assertion vtocl2 ψ

Proof

Step Hyp Ref Expression
1 vtocl2.1 AV
2 vtocl2.2 BV
3 vtocl2.3 x=Ay=Bφψ
4 vtocl2.4 φ
5 4 a1i y=Bφ
6 3 pm5.74da x=Ay=Bφy=Bψ
7 1 6 5 vtocl y=Bψ
8 5 7 2thd y=Bφψ
9 2 8 4 vtocl ψ