MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  vtoclg1f Structured version   Unicode version

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
StepHypRef 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 ) )
64, 5mpbii 211 . . . 4  |-  ( x  =  A  ->  ps )
73, 6exlimi 1850 . . 3  |-  ( E. x  x  =  A  ->  ps )
82, 7sylbi 195 . 2  |-  ( A  e.  _V  ->  ps )
91, 8syl 16 1  |-  ( A  e.  V  ->  ps )
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator