Theorem dtrucor3 48532

Description: An example of how ax-5 1909 without a distinct variable condition causes paradox in models of at least two objects. The hypothesis "dtrucor3.1" is provable from dtru 5456 in the ZF set theory. axc16nf 2264 and euae 2663 demonstrate that the violation of dtru 5456 leads to a model with only one object assuming its existence (ax-6 1967). The conclusion is also provable in the empty model ( see emptyal 1907). See also nf5 2286 and nf5i 2146 for the relation between unconditional ax-5 1909 and being not free. (Contributed by Zhi Wang, 23-Sep-2024.)

Hypotheses

Ref	Expression
dtrucor3.1	⊢ ¬ ∀𝑥 𝑥 = 𝑦
dtrucor3.2	⊢ (𝑥 = 𝑦 → ∀𝑥 𝑥 = 𝑦)

Assertion

Ref	Expression
dtrucor3	⊢ ∀𝑥 𝑥 = 𝑦

Distinct variable group:   𝑥,𝑦

Proof of Theorem dtrucor3

Step	Hyp	Ref	Expression
1		ax6ev 1969	. 2 ⊢ ∃𝑥 𝑥 = 𝑦
2		dtrucor3.1	. . . 4 ⊢ ¬ ∀𝑥 𝑥 = 𝑦
3		dtrucor3.2	. . . 4 ⊢ (𝑥 = 𝑦 → ∀𝑥 𝑥 = 𝑦)
4	2, 3	mto 197	. . 3 ⊢ ¬ 𝑥 = 𝑦
5	4	nex 1798	. 2 ⊢ ¬ ∃𝑥 𝑥 = 𝑦
6	1, 5	pm2.24ii 120	1 ⊢ ∀𝑥 𝑥 = 𝑦

Syntax hints:  ¬ wn 3  ∀wal 1535  ∃wex 1777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-6 1967

This theorem depends on definitions:  df-bi 207  df-ex 1778

This theorem is referenced by: (None)