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

Theorem vtoclg1f 3166
Description: Version of vtoclgf 3165 with one non-freeness hypothesis replaced with a dv condition, thus avoiding dependency on ax-11 1842 and ax-13 1999. (Contributed by BJ, 1-May-2019.)
Hypotheses
Ref Expression
vtoclg1f.nf
vtoclg1f.maj
vtoclg1f.min
Assertion
Ref Expression
vtoclg1f
Distinct variable group:   ,

Proof of Theorem vtoclg1f
StepHypRef Expression
1 elex 3118 . 2
2 isset 3113 . . 3
3 vtoclg1f.nf . . . 4
4 vtoclg1f.min . . . . 5
5 vtoclg1f.maj . . . . 5
64, 5mpbii 211 . . . 4
73, 6exlimi 1912 . . 3
82, 7sylbi 195 . 2
91, 8syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  E.wex 1612  F/wnf 1616  e.wcel 1818   cvv 3109
This theorem is referenced by:  vtoclg  3167  ceqsexg  3231  mob  3281  opeliunxp2  5146  fvopab5  5979  cnextfvval  20565  dvfsumlem2  22428  dvfsumlem4  22430  fmul01  31574  fmuldfeq  31577  fmul01lt1lem1  31578  cncfiooicclem1  31696  stoweidlem3  31785  stoweidlem26  31808  stoweidlem31  31813  stoweidlem43  31825  stoweidlem51  31833  fourierdlem86  31975  fourierdlem89  31978  fourierdlem91  31980  bnj981  34008
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-12 1854  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-v 3111
  Copyright terms: Public domain W3C validator