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

Theorem vtoclg1f 3163
Description: Version of vtoclgf 3162 with one non-freeness hypothesis replaced with a dv condition, thus avoiding dependency on ax-11 1847 and ax-13 2004. (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 3115 . 2  |-  ( A  e.  V  ->  A  e.  _V )
2 isset 3110 . . 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 1917 . . 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 1398   E.wex 1617   F/wnf 1621    e. wcel 1823   _Vcvv 3106
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-12 1859  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-v 3108
This theorem is referenced by:  vtoclg  3164  ceqsexg  3228  mob  3278  opeliunxp2  5130  fvopab5  5955  cnextfvval  20731  dvfsumlem2  22594  dvfsumlem4  22596  fmul01  31813  fmuldfeq  31816  fmul01lt1lem1  31817  cncfiooicclem1  31935  stoweidlem3  32024  stoweidlem26  32047  stoweidlem31  32052  stoweidlem43  32064  stoweidlem51  32072  fourierdlem86  32214  fourierdlem89  32217  fourierdlem91  32219  bnj981  34409
  Copyright terms: Public domain W3C validator