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

Theorem vtoclg1f 3523
Description: Version of vtoclgf 3522 with one nonfreeness hypothesis replaced with a disjoint variable condition, thus avoiding dependency on ax-10 2138 and ax-11 2155. (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 2816 . 2 (𝐴𝑉 → ∃𝑥 𝑥 = 𝐴)
2 vtoclg1f.nf . . 3 𝑥𝜓
3 vtoclg1f.min . . . 4 𝜑
4 vtoclg1f.maj . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
53, 4mpbii 232 . . 3 (𝑥 = 𝐴𝜓)
62, 5exlimi 2211 . 2 (∃𝑥 𝑥 = 𝐴𝜓)
71, 6syl 17 1 (𝐴𝑉𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1542  wex 1782  wnf 1786  wcel 2107
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-12 2172
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-clel 2811
This theorem is referenced by:  vtoclgOLDOLD  3526  ceqsexg  3604  elabgOLD  3630  mob  3676  opeliunxp2  5795  fvopab5  6981  opeliunxp2f  8142  fprodsplit1f  15878  cnextfvval  23432  dvfsumlem2  25407  dvfsumlem4  25409  bnj981  33619  dmrelrnrel  43534  fmul01  43907  fmuldfeq  43910  fmul01lt1lem1  43911  stoweidlem3  44330  stoweidlem26  44353  stoweidlem31  44358  stoweidlem43  44370  stoweidlem51  44378  fourierdlem86  44519  fourierdlem89  44522  fourierdlem91  44524  salpreimagelt  45034  salpreimalegt  45036
  Copyright terms: Public domain W3C validator