Theorem dtruALT 5392

Description: Alternate proof of dtru 5442 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 3595 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 5363	. . . 4 ⊢ (𝑦 = ∅ → ¬ 𝑦 = {∅})
2		p0ex 5388	. . . . 5 ⊢ {∅} ∈ V
3		eqeq2 2740	. . . . . 6 ⊢ (𝑥 = {∅} → (𝑦 = 𝑥 ↔ 𝑦 = {∅}))
4	3	notbid 317	. . . . 5 ⊢ (𝑥 = {∅} → (¬ 𝑦 = 𝑥 ↔ ¬ 𝑦 = {∅}))
5	2, 4	spcev 3595	. . . 4 ⊢ (¬ 𝑦 = {∅} → ∃𝑥 ¬ 𝑦 = 𝑥)
6	1, 5	syl 17	. . 3 ⊢ (𝑦 = ∅ → ∃𝑥 ¬ 𝑦 = 𝑥)
7		0ex 5311	. . . 4 ⊢ ∅ ∈ V
8		eqeq2 2740	. . . . 5 ⊢ (𝑥 = ∅ → (𝑦 = 𝑥 ↔ 𝑦 = ∅))
9	8	notbid 317	. . . 4 ⊢ (𝑥 = ∅ → (¬ 𝑦 = 𝑥 ↔ ¬ 𝑦 = ∅))
10	7, 9	spcev 3595	. . 3 ⊢ (¬ 𝑦 = ∅ → ∃𝑥 ¬ 𝑦 = 𝑥)
11	6, 10	pm2.61i 182	. 2 ⊢ ∃𝑥 ¬ 𝑦 = 𝑥
12		exnal 1821	. . 3 ⊢ (∃𝑥 ¬ 𝑦 = 𝑥 ↔ ¬ ∀𝑥 𝑦 = 𝑥)
13		eqcom 2735	. . . 4 ⊢ (𝑦 = 𝑥 ↔ 𝑥 = 𝑦)
14	13	albii 1813	. . 3 ⊢ (∀𝑥 𝑦 = 𝑥 ↔ ∀𝑥 𝑥 = 𝑦)
15	12, 14	xchbinx 333	. 2 ⊢ (∃𝑥 ¬ 𝑦 = 𝑥 ↔ ¬ ∀𝑥 𝑥 = 𝑦)
16	11, 15	mpbi 229	1 ⊢ ¬ ∀𝑥 𝑥 = 𝑦

Syntax hints:  ¬ wn 3  ∀wal 1531   = wceq 1533  ∃wex 1773  ∅c0 4326  {csn 4632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pow 5369

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-ne 2938  df-v 3475  df-dif 3952  df-in 3956  df-ss 3966  df-nul 4327  df-pw 4608  df-sn 4633

This theorem is referenced by: (None)