Theorem vtoclgf 2970

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

Hypotheses

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

Assertion

Ref	Expression
vtoclgf	|- ( A e. V -> ps )

Proof of Theorem vtoclgf

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

Syntax hints:   -> wi 4   <-> wb 177   E.wex 1547   F/wnf 1550   = wceq 1649   e. wcel 1721   F/_wnfc 2527   _Vcvv 2916

This theorem is referenced by:  vtoclg  2971  vtocl2gf  2973  vtocl3gf  2974  vtoclgaf  2976  ceqsexg  3027  elabgf  3040  mob  3076  opeliunxp2  4972  fvopab5  6493  cnextfvval  18049  dvfsumlem2  19864  dvfsumlem4  19866  ssiun2sf  23963  subtr  26207  subtr2  26208  fmul01  27577  fmuldfeqlem1  27579  fmuldfeq  27580  fmul01lt1lem1  27581  climsuse  27601  stoweidlem3  27619  stoweidlem26  27642  stoweidlem31  27647  stoweidlem43  27659  stoweidlem51  27667  stoweidlem59  27675

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918