Theorem noel 3516

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 3345	. . 3 ⊢ (𝐴 ∈ (V ∖ V) → 𝐴 ∈ V)
2		eldifn 3346	. . 3 ⊢ (𝐴 ∈ (V ∖ V) → ¬ 𝐴 ∈ V)
3	1, 2	pm2.65i 644	. 2 ⊢ ¬ 𝐴 ∈ (V ∖ V)
4		df-nul 3513	. . 3 ⊢ ∅ = (V ∖ V)
5	4	eleq2i 2301	. 2 ⊢ (𝐴 ∈ ∅ ↔ 𝐴 ∈ (V ∖ V))
6	3, 5	mtbir 678	1 ⊢ ¬ 𝐴 ∈ ∅

Syntax hints:  ¬ wn 3   ∈ wcel 2205  Vcvv 2815   ∖ cdif 3211  ∅c0 3512

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-dif 3216  df-nul 3513

This theorem is referenced by:  nel02  3517  n0i  3518  n0rf  3525  rex0  3530  eq0  3531  abvor0dc  3536  rab0  3541  un0  3546  in0  3547  0ss  3551  disj  3561  ral0  3615  rabsnifsb  3762  rabsnif  3763  int0  3968  iun0  4053  0iun  4054  br0  4163  exmid01  4316  nlim0  4520  nsuceq0g  4544  ordtriexmidlem  4646  ordtriexmidlem2  4647  ordtriexmid  4648  ontriexmidim  4649  ordtri2or2exmidlem  4653  onsucelsucexmidlem  4656  reg2exmidlema  4661  reg3exmidlemwe  4706  nn0eln0  4747  0xp  4835  dm0  4975  dm0rn0  4978  reldm0  4979  cnv0  5171  co02  5281  0fv  5713  acexmidlema  6049  acexmidlemb  6050  acexmidlemab  6052  mpo0  6131  nnsucelsuc  6737  nnsucuniel  6741  nnmordi  6762  nnaordex  6774  0er  6814  elssdc  7175  fissfi  7229  fidcenumlemrk  7237  nnnninfeq  7432  iftrueb01  7546  pw1if  7548  elni2  7645  nlt1pig  7672  0npr  7814  fzm1  10456  frec2uzltd  10789  0tonninf  10826  sum0  12099  fsumsplit  12118  sumsplitdc  12143  fsum2dlemstep  12145  prod0  12296  fprod2dlemstep  12333  ballotfilemcdc  13167  ennnfonelem1  13242  0g0  13639  0ntop  14998  0met  15375  lgsdir2lem3  16029  vtxdg0v  16415  clwwlkn0  16529  clwwlknnn  16533  clwwlk0on0  16552  eupth2lem1  16579  eupth2lem3lem4fi  16594  bdcnul  16761  bj-nnelirr  16849  nnnninfex  16926