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

Theorem noel 3228
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 3066 . . 3 (𝐴 ∈ (V ∖ V) → 𝐴 ∈ V)
2 eldifn 3067 . . 3 (𝐴 ∈ (V ∖ V) → ¬ 𝐴 ∈ V)
31, 2pm2.65i 568 . 2 ¬ 𝐴 ∈ (V ∖ V)
4 df-nul 3225 . . 3 ∅ = (V ∖ V)
54eleq2i 2104 . 2 (𝐴 ∈ ∅ ↔ 𝐴 ∈ (V ∖ V))
63, 5mtbir 596 1 ¬ 𝐴 ∈ ∅
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wcel 1393  Vcvv 2557  cdif 2914  c0 3224
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-v 2559  df-dif 2920  df-nul 3225
This theorem is referenced by:  n0i  3229  n0rf  3233  rex0  3238  eq0  3239  abvor0dc  3242  rab0  3246  un0  3251  in0  3252  0ss  3255  disj  3268  ral0  3322  int0  3629  iun0  3713  0iun  3714  nlim0  4131  nsuceq0g  4155  ordtriexmidlem  4245  ordtriexmidlem2  4246  ordtriexmid  4247  ordtri2or2exmidlem  4251  onsucelsucexmidlem  4254  reg2exmidlema  4259  reg3exmidlemwe  4303  nn0eln0  4341  0xp  4420  dm0  4549  dm0rn0  4552  reldm0  4553  cnv0  4727  co02  4834  0fv  5208  acexmidlema  5503  acexmidlemb  5504  acexmidlemab  5506  mpt20  5574  nnsucelsuc  6070  nnmordi  6089  nnaordex  6100  0er  6140  elni2  6410  nlt1pig  6437  0npr  6579  fzm1  8960  frec2uzltd  9163  bdcnul  9959  bj-nnelirr  10052
  Copyright terms: Public domain W3C validator