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

Theorem noel 3256
Description: The empty set has no elements. Theorem 6.14 of [Quine] p. 44. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Mario Carneiro, 1-Sep-2015.)
Assertion
Ref Expression
noel ¬ 𝐴 ∈ ∅

Proof of Theorem noel
StepHypRef Expression
1 eldifi 3094 . . 3 (𝐴 ∈ (V ∖ V) → 𝐴 ∈ V)
2 eldifn 3095 . . 3 (𝐴 ∈ (V ∖ V) → ¬ 𝐴 ∈ V)
31, 2pm2.65i 578 . 2 ¬ 𝐴 ∈ (V ∖ V)
4 df-nul 3253 . . 3 ∅ = (V ∖ V)
54eleq2i 2120 . 2 (𝐴 ∈ ∅ ↔ 𝐴 ∈ (V ∖ V))
63, 5mtbir 606 1 ¬ 𝐴 ∈ ∅
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wcel 1409  Vcvv 2574  cdif 2942  c0 3252
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 554  ax-in2 555  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-v 2576  df-dif 2948  df-nul 3253
This theorem is referenced by:  n0i  3257  n0rf  3261  rex0  3266  eq0  3267  abvor0dc  3270  rab0  3274  un0  3279  in0  3280  0ss  3283  disj  3296  ral0  3350  int0  3657  iun0  3741  0iun  3742  nlim0  4159  nsuceq0g  4183  ordtriexmidlem  4273  ordtriexmidlem2  4274  ordtriexmid  4275  ordtri2or2exmidlem  4279  onsucelsucexmidlem  4282  reg2exmidlema  4287  reg3exmidlemwe  4331  nn0eln0  4369  0xp  4448  dm0  4577  dm0rn0  4580  reldm0  4581  cnv0  4755  co02  4862  0fv  5236  acexmidlema  5531  acexmidlemb  5532  acexmidlemab  5534  mpt20  5602  nnsucelsuc  6101  nnmordi  6120  nnaordex  6131  0er  6171  elni2  6470  nlt1pig  6497  0npr  6639  fzm1  9064  frec2uzltd  9353  bdcnul  10372  bj-nnelirr  10465
  Copyright terms: Public domain W3C validator