Theorem noel 3367

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

Step	Hyp	Ref	Expression
1		eldifi 3198	. . 3 ⊢ (𝐴 ∈ (V ∖ V) → 𝐴 ∈ V)
2		eldifn 3199	. . 3 ⊢ (𝐴 ∈ (V ∖ V) → ¬ 𝐴 ∈ V)
3	1, 2	pm2.65i 628	. 2 ⊢ ¬ 𝐴 ∈ (V ∖ V)
4		df-nul 3364	. . 3 ⊢ ∅ = (V ∖ V)
5	4	eleq2i 2206	. 2 ⊢ (𝐴 ∈ ∅ ↔ 𝐴 ∈ (V ∖ V))
6	3, 5	mtbir 660	1 ⊢ ¬ 𝐴 ∈ ∅

Syntax hints:  ¬ wn 3   ∈ wcel 1480  Vcvv 2686   ∖ cdif 3068  ∅c0 3363

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 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-v 2688  df-dif 3073  df-nul 3364

This theorem is referenced by:  n0i  3368  n0rf  3375  rex0  3380  eq0  3381  abvor0dc  3386  rab0  3391  un0  3396  in0  3397  0ss  3401  disj  3411  ral0  3464  int0  3785  iun0  3869  0iun  3870  br0  3976  exmid01  4121  nlim0  4316  nsuceq0g  4340  ordtriexmidlem  4435  ordtriexmidlem2  4436  ordtriexmid  4437  ordtri2or2exmidlem  4441  onsucelsucexmidlem  4444  reg2exmidlema  4449  reg3exmidlemwe  4493  nn0eln0  4533  0xp  4619  dm0  4753  dm0rn0  4756  reldm0  4757  cnv0  4942  co02  5052  0fv  5456  acexmidlema  5765  acexmidlemb  5766  acexmidlemab  5768  mpo0  5841  nnsucelsuc  6387  nnsucuniel  6391  nnmordi  6412  nnaordex  6423  0er  6463  fidcenumlemrk  6842  elni2  7122  nlt1pig  7149  0npr  7291  fzm1  9880  frec2uzltd  10176  0tonninf  10212  sum0  11157  fsumsplit  11176  sumsplitdc  11201  fsum2dlemstep  11203  ennnfonelem1  11920  0ntop  12174  0met  12553  bdcnul  13063  bj-nnelirr  13151  nninfalllemn  13202