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

Theorem vtoclg1f 3533
Description: Version of vtoclgf 3532 with one nonfreeness hypothesis replaced with a disjoint variable condition, thus avoiding dependency on ax-10 2178 and ax-11 2194. (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 elisset 2844 . 2 (𝐴𝑉 → ∃𝑥 𝑥 = 𝐴)
2 vtoclg1f.nf . . 3 𝑥𝜓
3 vtoclg1f.min . . . 4 𝜑
4 vtoclg1f.maj . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
53, 4mpbii 236 . . 3 (𝑥 = 𝐴𝜓)
62, 5exlimi 2255 . 2 (∃𝑥 𝑥 = 𝐴𝜓)
71, 6syl 18 1 (𝐴𝑉𝜓)
Colors of variables:    wff setvar class
This proof depends on syntax axioms:  wi 4  wb 209   = wceq 1570  wex 1812  wnf 1816  wcel 2145
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-12 2215
This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2741  df-clel 2837
This theorem is used by:  ceqsexg  3610  mob  3678  opeliunxp2  5822  fvopab5  7024  opeliunxp2f  8212  fprodsplit1f  16083  cnextfvval  24297  dvfsumlem2  26261  dvfsumlem4  26263  bnj981  35467  dmrelrnrel  46064  fmul01  46418  fmuldfeq  46421  fmul01lt1lem1  46422  fprodcnlem  46437  stoweidlem3  46839  stoweidlem26  46862  stoweidlem31  46867  stoweidlem43  46879  stoweidlem51  46887  fourierdlem86  47028  fourierdlem89  47031  fourierdlem91  47033  sge0f1o  47218  salpreimagelt  47543  salpreimalegt  47545
  Copyright terms: Public domain W3C validator