Description: Demonstration of a theorem that requires the setvar variables x and y to be disjoint (but without any other disjointness conditions, and in particular, none on z ).
That theorem bundles the theorems ( |- E. x ( x = y -> z e. x ) with x , y , z disjoint), often called its "principal instance", and the two "degenerate instances" ( |- E. x ( x = y -> x e. x ) with x , y disjoint) and ( |- E. x ( x = y -> y e. x ) with x , y disjoint).
Compare with dvdemo2 , 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 for details on the "disjoint variable" mechanism. (The verb "bundle" to express this phenomenon was introduced by Raph Levien.)
Note that dvdemo1 is partially bundled, in that the pairs of setvar variables x , z and y , z need not be disjoint, and in spite of that, its proof does not require ax-11 nor ax-13 . (Contributed by NM, 1-Dec-2006) (Revised by BJ, 13-Jan-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | dvdemo1 | ⊢ ∃ 𝑥 ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑥 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dtru | ⊢ ¬ ∀ 𝑥 𝑥 = 𝑦 | |
| 2 | exnal | ⊢ ( ∃ 𝑥 ¬ 𝑥 = 𝑦 ↔ ¬ ∀ 𝑥 𝑥 = 𝑦 ) | |
| 3 | 1 2 | mpbir | ⊢ ∃ 𝑥 ¬ 𝑥 = 𝑦 |
| 4 | pm2.21 | ⊢ ( ¬ 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑥 ) ) | |
| 5 | 3 4 | eximii | ⊢ ∃ 𝑥 ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑥 ) |