Theorem dvdemo1 5379

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

Note that dvdemo1 5379 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 2155 nor ax-13 2375. (Contributed by NM, 1-Dec-2006.) (Revised by BJ, 13-Jan-2024.)

Assertion

Ref	Expression
dvdemo1	⊢ ∃𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥)

Distinct variable group:   𝑥,𝑦

Proof of Theorem dvdemo1

Step	Hyp	Ref	Expression
1		dtruALT2 5376	. . 3 ⊢ ¬ ∀𝑥 𝑥 = 𝑦
2		exnal 1824	. . 3 ⊢ (∃𝑥 ¬ 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦)
3	1, 2	mpbir 231	. 2 ⊢ ∃𝑥 ¬ 𝑥 = 𝑦
4		pm2.21 123	. 2 ⊢ (¬ 𝑥 = 𝑦 → (𝑥 = 𝑦 → 𝑧 ∈ 𝑥))
5	3, 4	eximii 1834	1 ⊢ ∃𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1535  ∃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 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-nul 5312  ax-pow 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777

This theorem is referenced by: (None)