Theorem vtoclg1f 3135

Description: Version of vtoclgf 3134 with one non-freeness hypothesis replaced with a dv condition, thus avoiding dependency on ax-11 1782 and ax-13 1955. (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 3087	. 2 |- ( A e. V -> A e. _V )
2		isset 3082	. . 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 211	. . . 4 |- ( x = A -> ps )
7	3, 6	exlimi 1850	. . 3 |- ( E. x x = A -> ps )
8	2, 7	sylbi 195	. 2 |- ( A e. _V -> ps )
9	1, 8	syl 16	1 |- ( A e. V -> ps )

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1370   E.wex 1587   F/wnf 1590   e. wcel 1758   _Vcvv 3078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-12 1794  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-v 3080

This theorem is referenced by:  vtoclg  3136  ceqsexg  3198  mob  3248  opeliunxp2  5087  fvopab5  5905  cnextfvval  19770  dvfsumlem2  21633  dvfsumlem4  21635  fmul01  29910  fmuldfeq  29913  fmul01lt1lem1  29914  stoweidlem3  29947  stoweidlem26  29970  stoweidlem31  29975  stoweidlem43  29987  stoweidlem51  29995