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

Theorem dtruex 4338
 Description: At least two sets exist (or in terms of first-order logic, the universe of discourse has two or more objects). Although dtruarb 3990 can also be summarized as "at least two sets exist", the difference is that dtruarb 3990 shows the existence of two sets which are not equal to each other, but this theorem says that given a specific 𝑦, we can construct a set 𝑥 which does not equal it. (Contributed by Jim Kingdon, 29-Dec-2018.)
Assertion
Ref Expression
dtruex 𝑥 ¬ 𝑥 = 𝑦
Distinct variable group:   𝑥,𝑦

Proof of Theorem dtruex
StepHypRef Expression
1 vex 2615 . . . . 5 𝑦 ∈ V
21snex 3984 . . . 4 {𝑦} ∈ V
32isseti 2618 . . 3 𝑥 𝑥 = {𝑦}
4 elirrv 4327 . . . . . . 7 ¬ 𝑦𝑦
5 vsnid 3450 . . . . . . . 8 𝑦 ∈ {𝑦}
6 eleq2 2146 . . . . . . . 8 (𝑦 = {𝑦} → (𝑦𝑦𝑦 ∈ {𝑦}))
75, 6mpbiri 166 . . . . . . 7 (𝑦 = {𝑦} → 𝑦𝑦)
84, 7mto 621 . . . . . 6 ¬ 𝑦 = {𝑦}
9 eqtr 2100 . . . . . 6 ((𝑦 = 𝑥𝑥 = {𝑦}) → 𝑦 = {𝑦})
108, 9mto 621 . . . . 5 ¬ (𝑦 = 𝑥𝑥 = {𝑦})
11 ancom 262 . . . . 5 ((𝑦 = 𝑥𝑥 = {𝑦}) ↔ (𝑥 = {𝑦} ∧ 𝑦 = 𝑥))
1210, 11mtbi 628 . . . 4 ¬ (𝑥 = {𝑦} ∧ 𝑦 = 𝑥)
1312imnani 658 . . 3 (𝑥 = {𝑦} → ¬ 𝑦 = 𝑥)
143, 13eximii 1534 . 2 𝑥 ¬ 𝑦 = 𝑥
15 equcom 1635 . . . 4 (𝑦 = 𝑥𝑥 = 𝑦)
1615notbii 627 . . 3 𝑦 = 𝑥 ↔ ¬ 𝑥 = 𝑦)
1716exbii 1537 . 2 (∃𝑥 ¬ 𝑦 = 𝑥 ↔ ∃𝑥 ¬ 𝑥 = 𝑦)
1814, 17mpbi 143 1 𝑥 ¬ 𝑥 = 𝑦
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   ∧ wa 102   = wceq 1285  ∃wex 1422   ∈ wcel 1434  {csn 3422 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3922  ax-pow 3974  ax-setind 4316 This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ne 2250  df-ral 2358  df-v 2614  df-dif 2986  df-in 2990  df-ss 2997  df-pw 3408  df-sn 3428 This theorem is referenced by:  dtru  4339  eunex  4340  brprcneu  5246
 Copyright terms: Public domain W3C validator