Metamath Proof Explorer


Theorem vtocl3

Description: Implicit substitution of classes for setvar variables. (Contributed by NM, 3-Jun-1995) (Proof shortened by Andrew Salmon, 8-Jun-2011) Avoid ax-10 and ax-11 . (Revised by Gino Giotto, 20-Aug-2023) (Proof shortened by Wolf Lammen, 23-Aug-2023)

Ref Expression
Hypotheses vtocl3.1 AV
vtocl3.2 BV
vtocl3.3 CV
vtocl3.4 x=Ay=Bz=Cφψ
vtocl3.5 φ
Assertion vtocl3 ψ

Proof

Step Hyp Ref Expression
1 vtocl3.1 AV
2 vtocl3.2 BV
3 vtocl3.3 CV
4 vtocl3.4 x=Ay=Bz=Cφψ
5 vtocl3.5 φ
6 5 a1i z=Cφ
7 4 3expa x=Ay=Bz=Cφψ
8 7 pm5.74da x=Ay=Bz=Cφz=Cψ
9 1 2 8 6 vtocl2 z=Cψ
10 6 9 2thd z=Cφψ
11 3 10 5 vtocl ψ