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

Theorem dvdemo1 5371
Description: Demonstration of a theorem that requires the setvar variables 𝑥 and 𝑦 to be disjoint (but without any other disjointness conditions, and in particular, none on 𝑧).

That theorem bundles the theorems (𝑥(𝑥 = 𝑦𝑧𝑥) with 𝑥, 𝑦, 𝑧 disjoint), often called its "principal instance", and the two "degenerate instances" (𝑥(𝑥 = 𝑦𝑥𝑥) with 𝑥, 𝑦 disjoint) and (𝑥(𝑥 = 𝑦𝑦𝑥) with 𝑥, 𝑦 disjoint).

Compare with dvdemo2 5372, which has the same principal instance and one common degenerate instance but crucially differs in the other degenerate instance.

See https://us.metamath.org/mpeuni/mmset.html#distinct 5372 for details on the "disjoint variable" mechanism. (The verb "bundle" to express this phenomenon was introduced by Raph Levien.)

Note that dvdemo1 5371 is partially bundled, in that the pairs of setvar variables 𝑥, 𝑧 and 𝑦, 𝑧 need not be disjoint, and in spite of that, its proof does not require ax-11 2154 nor ax-13 2371. (Contributed by NM, 1-Dec-2006.) (Revised by BJ, 13-Jan-2024.)

Assertion
Ref Expression
dvdemo1 𝑥(𝑥 = 𝑦𝑧𝑥)
Distinct variable group:   𝑥,𝑦

Proof of Theorem dvdemo1
StepHypRef Expression
1 dtruALT2 5368 . . 3 ¬ ∀𝑥 𝑥 = 𝑦
2 exnal 1829 . . 3 (∃𝑥 ¬ 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦)
31, 2mpbir 230 . 2 𝑥 ¬ 𝑥 = 𝑦
4 pm2.21 123 . 2 𝑥 = 𝑦 → (𝑥 = 𝑦𝑧𝑥))
53, 4eximii 1839 1 𝑥(𝑥 = 𝑦𝑧𝑥)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1539  wex 1781
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-nul 5306  ax-pow 5363
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator