Theorem noel 3451

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 3282	. . 3 ⊢ (𝐴 ∈ (V ∖ V) → 𝐴 ∈ V)
2		eldifn 3283	. . 3 ⊢ (𝐴 ∈ (V ∖ V) → ¬ 𝐴 ∈ V)
3	1, 2	pm2.65i 640	. 2 ⊢ ¬ 𝐴 ∈ (V ∖ V)
4		df-nul 3448	. . 3 ⊢ ∅ = (V ∖ V)
5	4	eleq2i 2260	. 2 ⊢ (𝐴 ∈ ∅ ↔ 𝐴 ∈ (V ∖ V))
6	3, 5	mtbir 672	1 ⊢ ¬ 𝐴 ∈ ∅

Syntax hints:  ¬ wn 3   ∈ wcel 2164  Vcvv 2760   ∖ cdif 3151  ∅c0 3447

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-dif 3156  df-nul 3448

This theorem is referenced by:  nel02  3452  n0i  3453  n0rf  3460  rex0  3465  eq0  3466  abvor0dc  3471  rab0  3476  un0  3481  in0  3482  0ss  3486  disj  3496  ral0  3549  int0  3885  iun0  3970  0iun  3971  br0  4078  exmid01  4228  nlim0  4426  nsuceq0g  4450  ordtriexmidlem  4552  ordtriexmidlem2  4553  ordtriexmid  4554  ontriexmidim  4555  ordtri2or2exmidlem  4559  onsucelsucexmidlem  4562  reg2exmidlema  4567  reg3exmidlemwe  4612  nn0eln0  4653  0xp  4740  dm0  4877  dm0rn0  4880  reldm0  4881  cnv0  5070  co02  5180  0fv  5591  acexmidlema  5910  acexmidlemb  5911  acexmidlemab  5913  mpo0  5989  nnsucelsuc  6546  nnsucuniel  6550  nnmordi  6571  nnaordex  6583  0er  6623  fidcenumlemrk  7015  nnnninfeq  7189  elni2  7376  nlt1pig  7403  0npr  7545  fzm1  10169  frec2uzltd  10477  0tonninf  10514  sum0  11534  fsumsplit  11553  sumsplitdc  11578  fsum2dlemstep  11580  prod0  11731  fprod2dlemstep  11768  ennnfonelem1  12567  0g0  12962  0ntop  14186  0met  14563  lgsdir2lem3  15187  if0ab  15367  bdcnul  15427  bj-nnelirr  15515