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

Theorem vtoclg1f 3092
Description: Version of vtoclgf 3091 with one non-freeness hypothesis replaced with a dv condition, thus avoiding dependency on ax-11 1937 and ax-13 2104. (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 3040 . 2  |-  ( A  e.  V  ->  A  e.  _V )
2 isset 3035 . . 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 216 . . . 4  |-  ( x  =  A  ->  ps )
73, 6exlimi 2015 . . 3  |-  ( E. x  x  =  A  ->  ps )
82, 7sylbi 200 . 2  |-  ( A  e.  _V  ->  ps )
91, 8syl 17 1  |-  ( A  e.  V  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    = wceq 1452   E.wex 1671   F/wnf 1675    e. wcel 1904   _Vcvv 3031
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-12 1950  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-v 3033
This theorem is referenced by:  vtoclg  3093  ceqsexg  3158  mob  3208  opeliunxp2  4978  fvopab5  5989  opeliunxp2f  6975  cnextfvval  21158  dvfsumlem2  23058  dvfsumlem4  23060  bnj981  29833  fmul01  37755  fmuldfeq  37758  fmul01lt1lem1  37759  cncfiooicclem1  37868  stoweidlem3  37975  stoweidlem26  37998  stoweidlem31  38004  stoweidlem43  38016  stoweidlem51  38024  fourierdlem86  38168  fourierdlem89  38171  fourierdlem91  38173
  Copyright terms: Public domain W3C validator