Theorem noel 3512

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

Syntax hints:  ¬ wn 3   ∈ wcel 2203  Vcvv 2813   ∖ cdif 3208  ∅c0 3508

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 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2815  df-dif 3213  df-nul 3509

This theorem is referenced by:  nel02  3513  n0i  3514  n0rf  3521  rex0  3526  eq0  3527  abvor0dc  3532  rab0  3537  un0  3542  in0  3543  0ss  3547  disj  3557  ral0  3611  rabsnifsb  3757  rabsnif  3758  int0  3963  iun0  4048  0iun  4049  br0  4158  exmid01  4311  nlim0  4515  nsuceq0g  4539  ordtriexmidlem  4641  ordtriexmidlem2  4642  ordtriexmid  4643  ontriexmidim  4644  ordtri2or2exmidlem  4648  onsucelsucexmidlem  4651  reg2exmidlema  4656  reg3exmidlemwe  4701  nn0eln0  4742  0xp  4830  dm0  4970  dm0rn0  4973  reldm0  4974  cnv0  5166  co02  5276  0fv  5708  acexmidlema  6041  acexmidlemb  6042  acexmidlemab  6044  mpo0  6123  nnsucelsuc  6724  nnsucuniel  6728  nnmordi  6749  nnaordex  6761  0er  6801  elssdc  7162  fissfi  7216  fidcenumlemrk  7224  nnnninfeq  7419  iftrueb01  7533  pw1if  7535  elni2  7629  nlt1pig  7656  0npr  7798  fzm1  10434  frec2uzltd  10765  0tonninf  10802  sum0  12074  fsumsplit  12093  sumsplitdc  12118  fsum2dlemstep  12120  prod0  12271  fprod2dlemstep  12308  ennnfonelem1  13158  0g0  13589  0ntop  14872  0met  15249  lgsdir2lem3  15903  vtxdg0v  16289  clwwlkn0  16403  clwwlknnn  16407  clwwlk0on0  16426  eupth2lem1  16453  eupth2lem3lem4fi  16468  bdcnul  16635  bj-nnelirr  16723  nnnninfex  16800