Metamath Proof Explorer


Theorem vtoclefex

Description: Implicit substitution of a class for a setvar variable. (Contributed by ML, 17-Oct-2020)

Ref Expression
Hypotheses vtoclefex.1 xφ
vtoclefex.3 x=Aφ
Assertion vtoclefex AVφ

Proof

Step Hyp Ref Expression
1 vtoclefex.1 xφ
2 vtoclefex.3 x=Aφ
3 2 ax-gen xx=Aφ
4 vtoclegft AVxφxx=Aφφ
5 1 3 4 mp3an23 AVφ