ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  dtruex Unicode version

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
StepHypRef Expression
1 vex 2774 . . . . 5  |-  y  e. 
_V
21snex 4228 . . . 4  |-  { y }  e.  _V
32isseti 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 } ) )
75, 6mpbiri 168 . . . . . . 7  |-  ( y  =  { y }  ->  y  e.  y )
84, 7mto 663 . . . . . 6  |-  -.  y  =  { y }
9 eqtr 2222 . . . . . 6  |-  ( ( y  =  x  /\  x  =  { y } )  ->  y  =  { y } )
108, 9mto 663 . . . . 5  |-  -.  (
y  =  x  /\  x  =  { y } )
11 ancom 266 . . . . 5  |-  ( ( y  =  x  /\  x  =  { y } )  <->  ( x  =  { y }  /\  y  =  x )
)
1210, 11mtbi 671 . . . 4  |-  -.  (
x  =  { y }  /\  y  =  x )
1312imnani 692 . . 3  |-  ( x  =  { y }  ->  -.  y  =  x )
143, 13eximii 1624 . 2  |-  E. x  -.  y  =  x
15 equcom 1728 . . . 4  |-  ( y  =  x  <->  x  =  y )
1615notbii 669 . . 3  |-  ( -.  y  =  x  <->  -.  x  =  y )
1716exbii 1627 . 2  |-  ( E. x  -.  y  =  x  <->  E. x  -.  x  =  y )
1814, 17mpbi 145 1  |-  E. x  -.  x  =  y
Colors of variables: wff set class
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
  Copyright terms: Public domain W3C validator