Theorem dtrucor3 49425

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

Syntax hints:  ¬ wn 3  ∀wal 1560  ∃wex 1801

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

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

This theorem is referenced by: (None)