Theorem dtruex 4606

Description: At least two sets exist (or in terms of first-order logic, the universe of discourse has two or more objects). Although dtruarb 4234 can also be summarized as "at least two sets exist", the difference is that dtruarb 4234 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	|- E. x -. x = y

Distinct variable group:   x, y

Proof of Theorem dtruex

Step	Hyp	Ref	Expression
1		vex 2774	. . . . 5 |- y e. _V
2	1	snex 4228	. . . 4 |- { y } e. _V
3	2	isseti 2779	. . 3 |- E. x x = { y }
4		elirrv 4595	. . . . . . 7 |- -. y e. y
5		vsnid 3664	. . . . . . . 8 |- y e. { y }
6		eleq2 2268	. . . . . . . 8 |- ( y = { y } -> ( y e. y <-> y e. { y } ) )
7	5, 6	mpbiri 168	. . . . . . 7 |- ( y = { y } -> y e. y )
8	4, 7	mto 663	. . . . . 6 |- -. y = { y }
9		eqtr 2222	. . . . . 6 |- ( ( y = x /\ x = { y } ) -> y = { y } )
10	8, 9	mto 663	. . . . 5 |- -. ( y = x /\ x = { y } )
11		ancom 266	. . . . 5 |- ( ( y = x /\ x = { y } ) <-> ( x = { y } /\ y = x ) )
12	10, 11	mtbi 671	. . . 4 |- -. ( x = { y } /\ y = x )
13	12	imnani 692	. . 3 |- ( x = { y } -> -. y = x )
14	3, 13	eximii 1624	. 2 |- E. x -. y = x
15		equcom 1728	. . . 4 |- ( y = x <-> x = y )
16	15	notbii 669	. . 3 |- ( -. y = x <-> -. x = y )
17	16	exbii 1627	. 2 |- ( E. x -. y = x <-> E. x -. x = y )
18	14, 17	mpbi 145	1 |- E. x -. x = y

Syntax hints:   -. wn 3   /\ wa 104   = wceq 1372   E.wex 1514   e. wcel 2175   {csn 3632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-14 2178  ax-ext 2186  ax-sep 4161  ax-pow 4217  ax-setind 4584

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ne 2376  df-ral 2488  df-v 2773  df-dif 3167  df-in 3171  df-ss 3178  df-pw 3617  df-sn 3638

This theorem is referenced by:  dtru  4607  eunex  4608  brprcneu  5568