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

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