Theorem vtoclg1f 3265

Description: Version of vtoclgf 3264 with one non-freeness hypothesis replaced with a dv condition, thus avoiding dependency on ax-11 2034 and ax-13 2246. (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 3212	. 2 |- ( A e. V -> A e. _V )
2		isset 3207	. . 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 223	. . . 4 |- ( x = A -> ps )
7	3, 6	exlimi 2086	. . 3 |- ( E. x x = A -> ps )
8	2, 7	sylbi 207	. 2 |- ( A e. _V -> ps )
9	1, 8	syl 17	1 |- ( A e. V -> ps )

Syntax hints:   -> wi 4   <-> wb 196   = wceq 1483   E.wex 1704   F/wnf 1708   e. wcel 1990   _Vcvv 3200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-12 2047  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-v 3202

This theorem is referenced by:  vtoclg  3266  ceqsexg  3334  mob  3388  opeliunxp2  5260  fvopab5  6309  opeliunxp2f  7336  cnextfvval  21869  dvfsumlem2  23790  dvfsumlem4  23792  bnj981  31020  dmrelrnrel  39419  fmul01  39812  fmuldfeq  39815  fmul01lt1lem1  39816  cncfiooicclem1  40106  stoweidlem3  40220  stoweidlem26  40243  stoweidlem31  40248  stoweidlem43  40260  stoweidlem51  40268  fourierdlem86  40409  fourierdlem89  40412  fourierdlem91  40414