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

Theorem vtoclg1f 3569
Description: Version of vtoclgf 3568 with one nonfreeness hypothesis replaced with a disjoint variable condition, thus avoiding dependency on ax-10 2140 and ax-11 2156. (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 2822 . 2 (𝐴𝑉 → ∃𝑥 𝑥 = 𝐴)
2 vtoclg1f.nf . . 3 𝑥𝜓
3 vtoclg1f.min . . . 4 𝜑
4 vtoclg1f.maj . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
53, 4mpbii 233 . . 3 (𝑥 = 𝐴𝜓)
62, 5exlimi 2216 . 2 (∃𝑥 𝑥 = 𝐴𝜓)
71, 6syl 17 1 (𝐴𝑉𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206   = wceq 1539  wex 1778  wnf 1782  wcel 2107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-12 2176
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-nf 1783  df-sb 2064  df-clab 2714  df-clel 2815
This theorem is referenced by:  ceqsexg  3652  mob  3722  opeliunxp2  5848  fvopab5  7048  opeliunxp2f  8236  fprodsplit1f  16027  cnextfvval  24074  dvfsumlem2  26068  dvfsumlem2OLD  26069  dvfsumlem4  26071  bnj981  34965  dmrelrnrel  45236  fmul01  45600  fmuldfeq  45603  fmul01lt1lem1  45604  fprodcnlem  45619  stoweidlem3  46023  stoweidlem26  46046  stoweidlem31  46051  stoweidlem43  46063  stoweidlem51  46071  fourierdlem86  46212  fourierdlem89  46215  fourierdlem91  46217  sge0f1o  46402  salpreimagelt  46727  salpreimalegt  46729
  Copyright terms: Public domain W3C validator