Theorem dtruALT 5385

Description: Alternate proof of dtru 5435 which requires more axioms but is shorter and may be easier to understand.

Assuming that ZF set theory is consistent, we cannot prove this theorem unless we specify that 𝑥 and 𝑦 be distinct. Specifically, Theorem spcev 3596 requires that 𝑥 must not occur in the subexpression ¬ 𝑦 = {∅} in step 4 nor in the subexpression ¬ 𝑦 = ∅ in step 9. The proof verifier will require that 𝑥 and 𝑦 be in a distinct variable group to ensure this. You can check this by deleting the $d statement in set.mm and rerunning the verifier, which will print a detailed explanation of the distinct variable violation. (Contributed by NM, 15-Jul-1994.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
dtruALT	⊢ ¬ ∀𝑥 𝑥 = 𝑦

Distinct variable group:   𝑥,𝑦

Proof of Theorem dtruALT

Step	Hyp	Ref	Expression
1		0inp0 5356	. . . 4 ⊢ (𝑦 = ∅ → ¬ 𝑦 = {∅})
2		p0ex 5381	. . . . 5 ⊢ {∅} ∈ V
3		eqeq2 2744	. . . . . 6 ⊢ (𝑥 = {∅} → (𝑦 = 𝑥 ↔ 𝑦 = {∅}))
4	3	notbid 317	. . . . 5 ⊢ (𝑥 = {∅} → (¬ 𝑦 = 𝑥 ↔ ¬ 𝑦 = {∅}))
5	2, 4	spcev 3596	. . . 4 ⊢ (¬ 𝑦 = {∅} → ∃𝑥 ¬ 𝑦 = 𝑥)
6	1, 5	syl 17	. . 3 ⊢ (𝑦 = ∅ → ∃𝑥 ¬ 𝑦 = 𝑥)
7		0ex 5306	. . . 4 ⊢ ∅ ∈ V
8		eqeq2 2744	. . . . 5 ⊢ (𝑥 = ∅ → (𝑦 = 𝑥 ↔ 𝑦 = ∅))
9	8	notbid 317	. . . 4 ⊢ (𝑥 = ∅ → (¬ 𝑦 = 𝑥 ↔ ¬ 𝑦 = ∅))
10	7, 9	spcev 3596	. . 3 ⊢ (¬ 𝑦 = ∅ → ∃𝑥 ¬ 𝑦 = 𝑥)
11	6, 10	pm2.61i 182	. 2 ⊢ ∃𝑥 ¬ 𝑦 = 𝑥
12		exnal 1829	. . 3 ⊢ (∃𝑥 ¬ 𝑦 = 𝑥 ↔ ¬ ∀𝑥 𝑦 = 𝑥)
13		eqcom 2739	. . . 4 ⊢ (𝑦 = 𝑥 ↔ 𝑥 = 𝑦)
14	13	albii 1821	. . 3 ⊢ (∀𝑥 𝑦 = 𝑥 ↔ ∀𝑥 𝑥 = 𝑦)
15	12, 14	xchbinx 333	. 2 ⊢ (∃𝑥 ¬ 𝑦 = 𝑥 ↔ ¬ ∀𝑥 𝑥 = 𝑦)
16	11, 15	mpbi 229	1 ⊢ ¬ ∀𝑥 𝑥 = 𝑦

Syntax hints:  ¬ wn 3  ∀wal 1539   = wceq 1541  ∃wex 1781  ∅c0 4321  {csn 4627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-v 3476  df-dif 3950  df-in 3954  df-ss 3964  df-nul 4322  df-pw 4603  df-sn 4628

This theorem is referenced by: (None)