Theorem dtrucor3 49605

Description: An example of how ax-5 1940 without a distinct variable condition causes paradox in models of at least two objects. The hypothesis "dtrucor3.1" is provable from dtru 5418 in the ZF set theory. axc16nf 2299 and euae 2687 demonstrate that the violation of dtru 5418 leads to a model with only one object assuming its existence (ax-6 1997). The conclusion is also provable in the empty model ( see emptyal 1938). See also nf5 2317 and nf5i 2181 for the relation between unconditional ax-5 1940 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 1999	. 2 ⊢ ∃𝑥 𝑥 = 𝑦
2		dtrucor3.1	. . . 4 ⊢ ¬ ∀𝑥 𝑥 = 𝑦
3		dtrucor3.2	. . . 4 ⊢ (𝑥 = 𝑦 → ∀𝑥 𝑥 = 𝑦)
4	2, 3	mto 200	. . 3 ⊢ ¬ 𝑥 = 𝑦
5	4	nex 1830	. 2 ⊢ ¬ ∃𝑥 𝑥 = 𝑦
6	1, 5	pm2.24ii 121	1 ⊢ ∀𝑥 𝑥 = 𝑦

This proof depends on syntax axioms:  ¬ wn 3  ∀wal 1568  ∃wex 1809

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-6 1997

This proof depends on definitions:  df-bi 210  df-ex 1810

This theorem is used by: (None)