Theorem dtrucor3 49303

Description: An example of how ax-5 1918 without a distinct variable condition causes paradox in models of at least two objects. The hypothesis "dtrucor3.1" is provable from dtru 5379 in the ZF set theory. axc16nf 2277 and euae 2665 demonstrate that the violation of dtru 5379 leads to a model with only one object assuming its existence (ax-6 1975). The conclusion is also provable in the empty model ( see emptyal 1916). See also nf5 2295 and nf5i 2159 for the relation between unconditional ax-5 1918 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 1977	. 2 ⊢ ∃𝑥 𝑥 = 𝑦
2		dtrucor3.1	. . . 4 ⊢ ¬ ∀𝑥 𝑥 = 𝑦
3		dtrucor3.2	. . . 4 ⊢ (𝑥 = 𝑦 → ∀𝑥 𝑥 = 𝑦)
4	2, 3	mto 199	. . 3 ⊢ ¬ 𝑥 = 𝑦
5	4	nex 1808	. 2 ⊢ ¬ ∃𝑥 𝑥 = 𝑦
6	1, 5	pm2.24ii 120	1 ⊢ ∀𝑥 𝑥 = 𝑦

Syntax hints:  ¬ wn 3  ∀wal 1546  ∃wex 1787

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

This theorem depends on definitions:  df-bi 209  df-ex 1788

This theorem is referenced by: (None)