Theorem vtoclg1f 3092

Description: Version of vtoclgf 3091 with one non-freeness hypothesis replaced with a dv condition, thus avoiding dependency on ax-11 1937 and ax-13 2104. (Contributed by BJ, 1-May-2019.)

Hypotheses

Ref	Expression
vtoclg1f.nf	|- F/ x ps
vtoclg1f.maj	|- ( x = A -> ( ph <-> ps ) )
vtoclg1f.min	|- ph

Assertion

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

Distinct variable group:   x, A

Allowed substitution hints:   ph( x)   ps( x)   V( x)

Proof of Theorem vtoclg1f

Step	Hyp	Ref	Expression
1		elex 3040	. 2 |- ( A e. V -> A e. _V )
2		isset 3035	. . 3 |- ( A e. _V <-> E. x x = A )
3		vtoclg1f.nf	. . . 4 |- F/ x ps
4		vtoclg1f.min	. . . . 5 |- ph
5		vtoclg1f.maj	. . . . 5 |- ( x = A -> ( ph <-> ps ) )
6	4, 5	mpbii 216	. . . 4 |- ( x = A -> ps )
7	3, 6	exlimi 2015	. . 3 |- ( E. x x = A -> ps )
8	2, 7	sylbi 200	. 2 |- ( A e. _V -> ps )
9	1, 8	syl 17	1 |- ( A e. V -> ps )

Syntax hints:   -> wi 4   <-> wb 189   = wceq 1452   E.wex 1671   F/wnf 1675   e. wcel 1904   _Vcvv 3031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-12 1950  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-v 3033

This theorem is referenced by:  vtoclg  3093  ceqsexg  3158  mob  3208  opeliunxp2  4978  fvopab5  5989  opeliunxp2f  6975  cnextfvval  21158  dvfsumlem2  23058  dvfsumlem4  23060  bnj981  29833  fmul01  37755  fmuldfeq  37758  fmul01lt1lem1  37759  cncfiooicclem1  37868  stoweidlem3  37975  stoweidlem26  37998  stoweidlem31  38004  stoweidlem43  38016  stoweidlem51  38024  fourierdlem86  38168  fourierdlem89  38171  fourierdlem91  38173