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

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

Note that dvdemo1 5266 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 2157 nor ax-13 2386. (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 5263 . . 3 ¬ ∀𝑥 𝑥 = 𝑦
2 exnal 1823 . . 3 (∃𝑥 ¬ 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦)
31, 2mpbir 233 . 2 𝑥 ¬ 𝑥 = 𝑦
4 pm2.21 123 . 2 𝑥 = 𝑦 → (𝑥 = 𝑦𝑧𝑥))
53, 4eximii 1833 1 𝑥(𝑥 = 𝑦𝑧𝑥)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1531  wex 1776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-12 2173  ax-nul 5202  ax-pow 5258
This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1536  df-ex 1777  df-nf 1781
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator