Theorem dtrucor3 46144

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

Syntax hints:  ¬ wn 3  ∀wal 1537  ∃wex 1782

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

This theorem depends on definitions:  df-bi 206  df-ex 1783

This theorem is referenced by: (None)