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
|- ( x = A -> ( ph <-> ps ) )
vtoclg.2
|- ph
Assertion vtoclg
|- ( A e. V -> ps )

Proof

Step Hyp Ref Expression
1 vtoclg.1
 |-  ( x = A -> ( ph <-> ps ) )
2 vtoclg.2
 |-  ph
3 2 1 mpbii
 |-  ( x = A -> ps )
4 3 vtocleg
 |-  ( A e. V -> ps )