Theorem noel 3498

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 3329	. . 3 ⊢ (𝐴 ∈ (V ∖ V) → 𝐴 ∈ V)
2		eldifn 3330	. . 3 ⊢ (𝐴 ∈ (V ∖ V) → ¬ 𝐴 ∈ V)
3	1, 2	pm2.65i 644	. 2 ⊢ ¬ 𝐴 ∈ (V ∖ V)
4		df-nul 3495	. . 3 ⊢ ∅ = (V ∖ V)
5	4	eleq2i 2298	. 2 ⊢ (𝐴 ∈ ∅ ↔ 𝐴 ∈ (V ∖ V))
6	3, 5	mtbir 677	1 ⊢ ¬ 𝐴 ∈ ∅

Syntax hints:  ¬ wn 3   ∈ wcel 2202  Vcvv 2802   ∖ cdif 3197  ∅c0 3494

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 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-dif 3202  df-nul 3495

This theorem is referenced by:  nel02  3499  n0i  3500  n0rf  3507  rex0  3512  eq0  3513  abvor0dc  3518  rab0  3523  un0  3528  in0  3529  0ss  3533  disj  3543  ral0  3596  rabsnifsb  3737  rabsnif  3738  int0  3942  iun0  4027  0iun  4028  br0  4137  exmid01  4288  nlim0  4491  nsuceq0g  4515  ordtriexmidlem  4617  ordtriexmidlem2  4618  ordtriexmid  4619  ontriexmidim  4620  ordtri2or2exmidlem  4624  onsucelsucexmidlem  4627  reg2exmidlema  4632  reg3exmidlemwe  4677  nn0eln0  4718  0xp  4806  dm0  4945  dm0rn0  4948  reldm0  4949  cnv0  5140  co02  5250  0fv  5677  acexmidlema  6009  acexmidlemb  6010  acexmidlemab  6012  mpo0  6091  nnsucelsuc  6659  nnsucuniel  6663  nnmordi  6684  nnaordex  6696  0er  6736  elssdc  7094  fidcenumlemrk  7153  nnnninfeq  7327  iftrueb01  7441  pw1if  7443  elni2  7534  nlt1pig  7561  0npr  7703  fzm1  10335  frec2uzltd  10666  0tonninf  10703  sum0  11967  fsumsplit  11986  sumsplitdc  12011  fsum2dlemstep  12013  prod0  12164  fprod2dlemstep  12201  ennnfonelem1  13046  0g0  13477  0ntop  14750  0met  15127  lgsdir2lem3  15778  vtxdg0v  16164  clwwlkn0  16278  clwwlknnn  16282  clwwlk0on0  16301  eupth2lem1  16328  eupth2lem3lem4fi  16343  if0ab  16452  bdcnul  16511  bj-nnelirr  16599  nnnninfex  16675