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

Theorem dfnul2 3392
 Description: Alternate definition of the empty set. Definition 5.14 of [TakeutiZaring] p. 20. (Contributed by NM, 26-Dec-1996.)
Assertion
Ref Expression
dfnul2 ∅ = {𝑥 ∣ ¬ 𝑥 = 𝑥}

Proof of Theorem dfnul2
StepHypRef Expression
1 df-nul 3391 . . . 4 ∅ = (V ∖ V)
21eleq2i 2221 . . 3 (𝑥 ∈ ∅ ↔ 𝑥 ∈ (V ∖ V))
3 eldif 3107 . . 3 (𝑥 ∈ (V ∖ V) ↔ (𝑥 ∈ V ∧ ¬ 𝑥 ∈ V))
4 pm3.24 683 . . . 4 ¬ (𝑥 ∈ V ∧ ¬ 𝑥 ∈ V)
5 eqid 2154 . . . . 5 𝑥 = 𝑥
65notnoti 635 . . . 4 ¬ ¬ 𝑥 = 𝑥
74, 62false 691 . . 3 ((𝑥 ∈ V ∧ ¬ 𝑥 ∈ V) ↔ ¬ 𝑥 = 𝑥)
82, 3, 73bitri 205 . 2 (𝑥 ∈ ∅ ↔ ¬ 𝑥 = 𝑥)
98abbi2i 2269 1 ∅ = {𝑥 ∣ ¬ 𝑥 = 𝑥}
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   ∧ wa 103   = wceq 1332   ∈ wcel 2125  {cab 2140  Vcvv 2709   ∖ cdif 3095  ∅c0 3390 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-10 1482  ax-11 1483  ax-i12 1484  ax-bndl 1486  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-ext 2136 This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1740  df-clab 2141  df-cleq 2147  df-clel 2150  df-nfc 2285  df-v 2711  df-dif 3100  df-nul 3391 This theorem is referenced by:  dfnul3  3393  rab0  3418  iotanul  5143
 Copyright terms: Public domain W3C validator