Metamath Proof Explorer


Theorem vtoclga

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 20-Aug-1995) Avoid ax-10 and ax-11 . (Revised by Gino Giotto, 20-Aug-2023)

Ref Expression
Hypotheses vtoclga.1 x = A φ ψ
vtoclga.2 x B φ
Assertion vtoclga A B ψ

Proof

Step Hyp Ref Expression
1 vtoclga.1 x = A φ ψ
2 vtoclga.2 x B φ
3 eleq1 x = A x B A B
4 3 1 imbi12d x = A x B φ A B ψ
5 4 2 vtoclg A B A B ψ
6 5 pm2.43i A B ψ