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

Theorem vtoclg1f 3255
Description: Version of vtoclgf 3254 with one non-freeness hypothesis replaced with a dv condition, thus avoiding dependency on ax-11 2031 and ax-13 2245. (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 3202 . 2 (𝐴𝑉𝐴 ∈ V)
2 isset 3197 . . 3 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
3 vtoclg1f.nf . . . 4 𝑥𝜓
4 vtoclg1f.min . . . . 5 𝜑
5 vtoclg1f.maj . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
64, 5mpbii 223 . . . 4 (𝑥 = 𝐴𝜓)
73, 6exlimi 2084 . . 3 (∃𝑥 𝑥 = 𝐴𝜓)
82, 7sylbi 207 . 2 (𝐴 ∈ V → 𝜓)
91, 8syl 17 1 (𝐴𝑉𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1480  wex 1701  wnf 1705  wcel 1987  Vcvv 3190
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-12 2044  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-v 3192
This theorem is referenced by:  vtoclg  3256  ceqsexg  3322  mob  3375  opeliunxp2  5230  fvopab5  6275  opeliunxp2f  7296  cnextfvval  21809  dvfsumlem2  23728  dvfsumlem4  23730  bnj981  30781  dmrelrnrel  38928  fmul01  39248  fmuldfeq  39251  fmul01lt1lem1  39252  cncfiooicclem1  39441  stoweidlem3  39557  stoweidlem26  39580  stoweidlem31  39585  stoweidlem43  39597  stoweidlem51  39605  fourierdlem86  39746  fourierdlem89  39749  fourierdlem91  39751
  Copyright terms: Public domain W3C validator