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

Theorem vtoclg1f 3466
Description: Version of vtoclgf 3465 with one non-freeness hypothesis replaced with a disjoint variable condition, thus avoiding dependency on ax-11 2150 and ax-13 2334. (Contributed by BJ, 1-May-2019.)
Hypotheses
Ref Expression
vtoclg1f.nf 𝑥𝜓
vtoclg1f.maj (𝑥 = 𝐴 → (𝜑𝜓))
vtoclg1f.min 𝜑
Assertion
Ref Expression
vtoclg1f (𝐴𝑉𝜓)
Distinct variable group:   𝑥,𝐴
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)   𝑉(𝑥)

Proof of Theorem vtoclg1f
StepHypRef Expression
1 elex 3414 . 2 (𝐴𝑉𝐴 ∈ V)
2 isset 3409 . . 3 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
3 vtoclg1f.nf . . . 4 𝑥𝜓
4 vtoclg1f.min . . . . 5 𝜑
5 vtoclg1f.maj . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
64, 5mpbii 225 . . . 4 (𝑥 = 𝐴𝜓)
73, 6exlimi 2203 . . 3 (∃𝑥 𝑥 = 𝐴𝜓)
82, 7sylbi 209 . 2 (𝐴 ∈ V → 𝜓)
91, 8syl 17 1 (𝐴𝑉𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198   = wceq 1601  wex 1823  wnf 1827  wcel 2107  Vcvv 3398
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-12 2163  ax-ext 2754
This theorem depends on definitions:  df-bi 199  df-an 387  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-v 3400
This theorem is referenced by:  vtoclg  3467  ceqsexg  3537  elabg  3556  mob  3600  opeliunxp2  5506  fvopab5  6572  opeliunxp2f  7618  fprodsplit1f  15123  cnextfvval  22277  dvfsumlem2  24227  dvfsumlem4  24229  bnj981  31619  dmrelrnrel  40340  fmul01  40720  fmuldfeq  40723  fmul01lt1lem1  40724  stoweidlem3  41147  stoweidlem26  41170  stoweidlem31  41175  stoweidlem43  41187  stoweidlem51  41195  fourierdlem86  41336  fourierdlem89  41339  fourierdlem91  41341
  Copyright terms: Public domain W3C validator