Theorem vtoclg1f 3106

Description: Version of vtoclgf 3105 with one non-freeness hypothesis replaced with a dv condition, thus avoiding dependency on ax-11 1920 and ax-13 2091. (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 3054	. 2 |- ( A e. V -> A e. _V )
2		isset 3049	. . 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 215	. . . 4 |- ( x = A -> ps )
7	3, 6	exlimi 1995	. . 3 |- ( E. x x = A -> ps )
8	2, 7	sylbi 199	. 2 |- ( A e. _V -> ps )
9	1, 8	syl 17	1 |- ( A e. V -> ps )

Syntax hints:   -> wi 4   <-> wb 188   = wceq 1444   E.wex 1663   F/wnf 1667   e. wcel 1887   _Vcvv 3045

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-12 1933  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-v 3047

This theorem is referenced by:  vtoclg  3107  ceqsexg  3170  mob  3220  opeliunxp2  4973  fvopab5  5974  opeliunxp2f  6956  cnextfvval  21080  dvfsumlem2  22979  dvfsumlem4  22981  bnj981  29761  fmul01  37658  fmuldfeq  37661  fmul01lt1lem1  37662  cncfiooicclem1  37771  stoweidlem3  37863  stoweidlem26  37886  stoweidlem31  37892  stoweidlem43  37904  stoweidlem51  37912  fourierdlem86  38056  fourierdlem89  38059  fourierdlem91  38061