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  6008  acexmidlemb  6009  acexmidlemab  6011  mpo0  6090  nnsucelsuc  6658  nnsucuniel  6662  nnmordi  6683  nnaordex  6695  0er  6735  elssdc  7093  fidcenumlemrk  7152  nnnninfeq  7326  iftrueb01  7440  pw1if  7442  elni2  7533  nlt1pig  7560  0npr  7702  fzm1  10334  frec2uzltd  10664  0tonninf  10701  sum0  11948  fsumsplit  11967  sumsplitdc  11992  fsum2dlemstep  11994  prod0  12145  fprod2dlemstep  12182  ennnfonelem1  13027  0g0  13458  0ntop  14730  0met  15107  lgsdir2lem3  15758  vtxdg0v  16144  clwwlkn0  16258  clwwlknnn  16262  clwwlk0on0  16281  eupth2lem1  16308  if0ab  16401  bdcnul  16460  bj-nnelirr  16548  nnnninfex  16624