Theorem noel 3496

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 3327	. . 3 ⊢ (𝐴 ∈ (V ∖ V) → 𝐴 ∈ V)
2		eldifn 3328	. . 3 ⊢ (𝐴 ∈ (V ∖ V) → ¬ 𝐴 ∈ V)
3	1, 2	pm2.65i 642	. 2 ⊢ ¬ 𝐴 ∈ (V ∖ V)
4		df-nul 3493	. . 3 ⊢ ∅ = (V ∖ V)
5	4	eleq2i 2296	. 2 ⊢ (𝐴 ∈ ∅ ↔ 𝐴 ∈ (V ∖ V))
6	3, 5	mtbir 675	1 ⊢ ¬ 𝐴 ∈ ∅

Syntax hints:  ¬ wn 3   ∈ wcel 2200  Vcvv 2800   ∖ cdif 3195  ∅c0 3492

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2802  df-dif 3200  df-nul 3493

This theorem is referenced by:  nel02  3497  n0i  3498  n0rf  3505  rex0  3510  eq0  3511  abvor0dc  3516  rab0  3521  un0  3526  in0  3527  0ss  3531  disj  3541  ral0  3594  rabsnifsb  3735  rabsnif  3736  int0  3940  iun0  4025  0iun  4026  br0  4135  exmid01  4286  nlim0  4489  nsuceq0g  4513  ordtriexmidlem  4615  ordtriexmidlem2  4616  ordtriexmid  4617  ontriexmidim  4618  ordtri2or2exmidlem  4622  onsucelsucexmidlem  4625  reg2exmidlema  4630  reg3exmidlemwe  4675  nn0eln0  4716  0xp  4804  dm0  4943  dm0rn0  4946  reldm0  4947  cnv0  5138  co02  5248  0fv  5673  acexmidlema  6004  acexmidlemb  6005  acexmidlemab  6007  mpo0  6086  nnsucelsuc  6654  nnsucuniel  6658  nnmordi  6679  nnaordex  6691  0er  6731  elssdc  7087  fidcenumlemrk  7144  nnnninfeq  7318  iftrueb01  7431  pw1if  7433  elni2  7524  nlt1pig  7551  0npr  7693  fzm1  10325  frec2uzltd  10655  0tonninf  10692  sum0  11939  fsumsplit  11958  sumsplitdc  11983  fsum2dlemstep  11985  prod0  12136  fprod2dlemstep  12173  ennnfonelem1  13018  0g0  13449  0ntop  14721  0met  15098  lgsdir2lem3  15749  vtxdg0v  16100  clwwlkn0  16203  clwwlknnn  16207  clwwlk0on0  16226  if0ab  16337  bdcnul  16396  bj-nnelirr  16484  nnnninfex  16560