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

Theorem vtoclg1f 3238
 Description: Version of vtoclgf 3237 with one non-freeness hypothesis replaced with a dv condition, thus avoiding dependency on ax-11 2021 and ax-13 2234. (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 3185 . 2 (𝐴𝑉𝐴 ∈ V)
2 isset 3180 . . 3 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
3 vtoclg1f.nf . . . 4 𝑥𝜓
4 vtoclg1f.min . . . . 5 𝜑
5 vtoclg1f.maj . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
64, 5mpbii 222 . . . 4 (𝑥 = 𝐴𝜓)
73, 6exlimi 2073 . . 3 (∃𝑥 𝑥 = 𝐴𝜓)
82, 7sylbi 206 . 2 (𝐴 ∈ V → 𝜓)
91, 8syl 17 1 (𝐴𝑉𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475  ∃wex 1695  Ⅎwnf 1699   ∈ wcel 1977  Vcvv 3173 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-v 3175 This theorem is referenced by:  vtoclg  3239  ceqsexg  3304  mob  3355  opeliunxp2  5182  fvopab5  6217  opeliunxp2f  7223  cnextfvval  21679  dvfsumlem2  23594  dvfsumlem4  23596  bnj981  30274  fmul01  38647  fmuldfeq  38650  fmul01lt1lem1  38651  cncfiooicclem1  38779  stoweidlem3  38896  stoweidlem26  38919  stoweidlem31  38924  stoweidlem43  38936  stoweidlem51  38944  fourierdlem86  39085  fourierdlem89  39088  fourierdlem91  39090
 Copyright terms: Public domain W3C validator