This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem vtoclgf

Description: Implicit substitution of a class for a setvar variable, with bound-variable hypotheses in place of disjoint variable restrictions. (Contributed by NM, 21-Sep-2003) (Proof shortened by Mario Carneiro, 10-Oct-2016)

Ref Expression
Hypotheses vtoclgf.1 
|- F/_ x A
vtoclgf.2 
|- F/ x ps
vtoclgf.3 
|- ( x = A -> ( ph <-> ps ) )
vtoclgf.4 
|- ph
Assertion vtoclgf 
|- ( A e. V -> ps )

Proof

Step Hyp Ref Expression
1 vtoclgf.1 
 |-  F/_ x A
2 vtoclgf.2 
 |-  F/ x ps
3 vtoclgf.3 
 |-  ( x = A -> ( ph <-> ps ) )
4 vtoclgf.4 
 |-  ph
5 elex 
 |-  ( A e. V -> A e. _V )
6 1 issetf 
 |-  ( A e. _V <-> E. x x = A )
7 4 3 mpbii 
 |-  ( x = A -> ps )
8 2 7 exlimi 
 |-  ( E. x x = A -> ps )
9 6 8 sylbi 
 |-  ( A e. _V -> ps )
10 5 9 syl 
 |-  ( A e. V -> ps )