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

Theorem dvdemo1 5265
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 5266, 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 5266 for details on the "disjoint variable" mechanism. (The verb "bundle" to express this phenomenon was introduced by Raph Levien.)

Note that dvdemo1 5265 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 2151 nor ax-13 2381. (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 dtru 5262 . . 3 ¬ ∀𝑥 𝑥 = 𝑦
2 exnal 1818 . . 3 (∃𝑥 ¬ 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦)
31, 2mpbir 232 . 2 𝑥 ¬ 𝑥 = 𝑦
4 pm2.21 123 . 2 𝑥 = 𝑦 → (𝑥 = 𝑦𝑧𝑥))
53, 4eximii 1828 1 𝑥(𝑥 = 𝑦𝑧𝑥)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1526  wex 1771
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-12 2167  ax-nul 5201  ax-pow 5257
This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1531  df-ex 1772  df-nf 1776
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator