Theorem vtoclgf 3104

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.)

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 3053	. 2 |- ( A e. V -> A e. _V )
2		vtoclgf.1	. . . 4 |- F/_ x A
3	2	issetf 3049	. . 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 215	. . . 4 |- ( x = A -> ps )
8	4, 7	exlimi 1994	. . 3 |- ( E. x x = A -> ps )
9	3, 8	sylbi 199	. 2 |- ( A e. _V -> ps )
10	1, 9	syl 17	1 |- ( A e. V -> ps )

Syntax hints:   -> wi 4   <-> wb 188   = wceq 1443   E.wex 1662   F/wnf 1666   e. wcel 1886   F/_wnfc 2578   _Vcvv 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-v 3046

This theorem is referenced by:  vtocl2gf  3108  vtocl3gf  3109  vtoclgaf  3111  elabgf  3182  fprodsplit1f  14037  ssiun2sf  28167  subtr  30963  subtr2  30964  supxrgere  37550  supxrgelem  37554  supxrge  37555  fsumsplit1  37645  fmuldfeqlem1  37654  climsuse  37681  dvnmptdivc  37807  dvmptfprodlem  37813  stoweidlem59  37914  fourierdlem31  37994  fourierdlem31OLD  37995  sge0f1o  38218  sge0fodjrnlem  38252