Metamath Proof Explorer


Theorem vtoclg

Description: Implicit substitution of a class expression for a setvar variable. (Contributed by NM, 17-Apr-1995) Avoid ax-12 . (Revised by SN, 20-Apr-2024) (Proof shortened by Wolf Lammen, 26-Jan-2025)

Ref Expression
Hypotheses vtoclg.1 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) )
vtoclg.2 𝜑
Assertion vtoclg ( 𝐴𝑉𝜓 )

Proof

Step Hyp Ref Expression
1 vtoclg.1 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) )
2 vtoclg.2 𝜑
3 2 1 mpbii ( 𝑥 = 𝐴𝜓 )
4 3 vtocleg ( 𝐴𝑉𝜓 )