Theorem dtrucor3

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

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

Proof

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