**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 5283, 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 5283 for details on
the "disjoint variable" mechanism. (The verb
"bundle" to express this
phenomenon was introduced by Raph Levien.)
Note that dvdemo1 5282 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 2160 nor ax-13 2373. (Contributed by
NM, 1-Dec-2006.) (Revised by BJ,
13-Jan-2024.) |