Theorem dtruex 4197

Description: At least two sets exist (or in terms of first-order logic, the universe of discourse has two or more objects). Although dtruarb 3895 can also be summarized as "at least two sets exist", the difference is that dtruarb 3895 shows the existence of two sets which are not equal to each other, but this theorem says that given a specific y, we can construct a set x which does not equal it. (Contributed by Jim Kingdon, 29-Dec-2018.)

Assertion

Ref	Expression
dtruex	⊢ ∃x ¬ x = y

Distinct variable group:   x,y

Proof of Theorem dtruex

Step	Hyp	Ref	Expression
1		vex 2537	. . . . 5 ⊢ y ∈ V
2		snexgOLD 3888	. . . . 5 ⊢ (y ∈ V → {y} ∈ V)
3	1, 2	ax-mp 7	. . . 4 ⊢ {y} ∈ V
4		isset 2538	. . . 4 ⊢ ({y} ∈ V ↔ ∃x x = {y})
5	3, 4	mpbi 133	. . 3 ⊢ ∃x x = {y}
6		elirr 4184	. . . . . . . 8 ⊢ ¬ y ∈ y
7		ssnid 3356	. . . . . . . . 9 ⊢ y ∈ {y}
8		eleq2 2084	. . . . . . . . 9 ⊢ (y = {y} → (y ∈ y ↔ y ∈ {y}))
9	7, 8	mpbiri 157	. . . . . . . 8 ⊢ (y = {y} → y ∈ y)
10	6, 9	mto 575	. . . . . . 7 ⊢ ¬ y = {y}
11		eqtr 2040	. . . . . . 7 ⊢ ((y = x ∧ x = {y}) → y = {y})
12	10, 11	mto 575	. . . . . 6 ⊢ ¬ (y = x ∧ x = {y})
13		ancom 253	. . . . . 6 ⊢ ((y = x ∧ x = {y}) ↔ (x = {y} ∧ y = x))
14	12, 13	mtbi 582	. . . . 5 ⊢ ¬ (x = {y} ∧ y = x)
15	14	imnani 612	. . . 4 ⊢ (x = {y} → ¬ y = x)
16	15	eximi 1475	. . 3 ⊢ (∃x x = {y} → ∃x ¬ y = x)
17	5, 16	ax-mp 7	. 2 ⊢ ∃x ¬ y = x
18		eqcom 2025	. . . 4 ⊢ (y = x ↔ x = y)
19	18	notbii 581	. . 3 ⊢ (¬ y = x ↔ ¬ x = y)
20	19	exbii 1480	. 2 ⊢ (∃x ¬ y = x ↔ ∃x ¬ x = y)
21	17, 20	mpbi 133	1 ⊢ ∃x ¬ x = y

Syntax hints:  ¬ wn 3   ∧ wa 97  ∃wex 1362   = wceq 1374   ∈ wcel 1376  Vcvv 2534  {csn 3328

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 532  ax-in2 533  ax-io 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1378  ax-10 1379  ax-11 1380  ax-i12 1381  ax-bnd 1382  ax-4 1383  ax-14 1388  ax-17 1402  ax-i9 1406  ax-ial 1411  ax-i5r 1412  ax-ext 2005  ax-sep 3828  ax-pow 3880  ax-setind 4180

This theorem depends on definitions:  df-bi 110  df-3an 878  df-tru 1232  df-nf 1330  df-sb 1629  df-clab 2010  df-cleq 2016  df-clel 2019  df-nfc 2150  df-ne 2189  df-ral 2288  df-v 2536  df-dif 2899  df-in 2903  df-ss 2910  df-pw 3314  df-sn 3334

This theorem is referenced by:  dtru  4198  eunex  4199  brprcneu  5073