Metamath Proof Explorer

Theorem vtocleg

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 21-Jun-1993)

Ref Expression
Hypothesis vtocleg.1 
|- ( x = A -> ph )
Assertion vtocleg 
|- ( A e. V -> ph )

Proof

Step Hyp Ref Expression
1 vtocleg.1 
 |-  ( x = A -> ph )
2 elisset 
 |-  ( A e. V -> E. x x = A )
3 1 exlimiv 
 |-  ( E. x x = A -> ph )
4 2 3 syl 
 |-  ( A e. V -> ph )