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

Theorem vtoclg1f 3504
Description: Version of vtoclgf 3503 with one nonfreeness hypothesis replaced with a disjoint variable condition, thus avoiding dependency on ax-11 2154 and ax-13 2372. (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 2820 . 2 (𝐴𝑉 → ∃𝑥 𝑥 = 𝐴)
2 vtoclg1f.nf . . 3 𝑥𝜓
3 vtoclg1f.min . . . 4 𝜑
4 vtoclg1f.maj . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
53, 4mpbii 232 . . 3 (𝑥 = 𝐴𝜓)
62, 5exlimi 2210 . 2 (∃𝑥 𝑥 = 𝐴𝜓)
71, 6syl 17 1 (𝐴𝑉𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1539  wex 1782  wnf 1786  wcel 2106
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-12 2171
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-clel 2816
This theorem is referenced by:  vtoclgOLD  3506  ceqsexg  3583  elabgOLD  3608  mob  3652  opeliunxp2  5747  fvopab5  6907  opeliunxp2f  8026  fprodsplit1f  15700  cnextfvval  23216  dvfsumlem2  25191  dvfsumlem4  25193  bnj981  32930  dmrelrnrel  42765  fmul01  43121  fmuldfeq  43124  fmul01lt1lem1  43125  stoweidlem3  43544  stoweidlem26  43567  stoweidlem31  43572  stoweidlem43  43584  stoweidlem51  43592  fourierdlem86  43733  fourierdlem89  43736  fourierdlem91  43738  salpreimagelt  44244  salpreimalegt  44246
  Copyright terms: Public domain W3C validator