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

Theorem vtoclg1f 3545
Description: Version of vtoclgf 3544 with one non-freeness hypothesis replaced with a disjoint variable condition, thus avoiding dependency on ax-11 2161 and ax-13 2390. (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 3484 . 2 (𝐴𝑉 → ∃𝑥 𝑥 = 𝐴)
2 vtoclg1f.nf . . 3 𝑥𝜓
3 vtoclg1f.min . . . 4 𝜑
4 vtoclg1f.maj . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
53, 4mpbii 235 . . 3 (𝑥 = 𝐴𝜓)
62, 5exlimi 2217 . 2 (∃𝑥 𝑥 = 𝐴𝜓)
71, 6syl 17 1 (𝐴𝑉𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208   = wceq 1537  wex 1780  wnf 1784  wcel 2114
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-12 2177  ax-ext 2792
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-nf 1785  df-cleq 2813  df-clel 2891
This theorem is referenced by:  vtoclgOLD  3547  ceqsexg  3625  elabg  3646  mob  3688  opeliunxp2  5685  fvopab5  6776  opeliunxp2f  7854  fprodsplit1f  15324  cnextfvval  22649  dvfsumlem2  24609  dvfsumlem4  24611  bnj981  32230  dmrelrnrel  41644  fmul01  42013  fmuldfeq  42016  fmul01lt1lem1  42017  stoweidlem3  42436  stoweidlem26  42459  stoweidlem31  42464  stoweidlem43  42476  stoweidlem51  42484  fourierdlem86  42625  fourierdlem89  42628  fourierdlem91  42630  salpreimagelt  43134  salpreimalegt  43136
  Copyright terms: Public domain W3C validator