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 dvdemo1 5300, 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 5300 for details on
the "disjoint variable" mechanism.
Note that dvdemo2 5301 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 any of the auxiliary axioms ax-10 2141,
ax-11 2158, ax-12 2175, ax-13 2374. (Contributed by NM, 1-Dec-2006.)
(Revised by BJ, 13-Jan-2024.) |