Theorem noel 3418

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 3249	. . 3 ⊢ (𝐴 ∈ (V ∖ V) → 𝐴 ∈ V)
2		eldifn 3250	. . 3 ⊢ (𝐴 ∈ (V ∖ V) → ¬ 𝐴 ∈ V)
3	1, 2	pm2.65i 634	. 2 ⊢ ¬ 𝐴 ∈ (V ∖ V)
4		df-nul 3415	. . 3 ⊢ ∅ = (V ∖ V)
5	4	eleq2i 2237	. 2 ⊢ (𝐴 ∈ ∅ ↔ 𝐴 ∈ (V ∖ V))
6	3, 5	mtbir 666	1 ⊢ ¬ 𝐴 ∈ ∅

Syntax hints:  ¬ wn 3   ∈ wcel 2141  Vcvv 2730   ∖ cdif 3118  ∅c0 3414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-dif 3123  df-nul 3415

This theorem is referenced by:  nel02  3419  n0i  3420  n0rf  3427  rex0  3432  eq0  3433  abvor0dc  3438  rab0  3443  un0  3448  in0  3449  0ss  3453  disj  3463  ral0  3516  int0  3845  iun0  3929  0iun  3930  br0  4037  exmid01  4184  nlim0  4379  nsuceq0g  4403  ordtriexmidlem  4503  ordtriexmidlem2  4504  ordtriexmid  4505  ontriexmidim  4506  ordtri2or2exmidlem  4510  onsucelsucexmidlem  4513  reg2exmidlema  4518  reg3exmidlemwe  4563  nn0eln0  4604  0xp  4691  dm0  4825  dm0rn0  4828  reldm0  4829  cnv0  5014  co02  5124  0fv  5531  acexmidlema  5844  acexmidlemb  5845  acexmidlemab  5847  mpo0  5923  nnsucelsuc  6470  nnsucuniel  6474  nnmordi  6495  nnaordex  6507  0er  6547  fidcenumlemrk  6931  nnnninfeq  7104  elni2  7276  nlt1pig  7303  0npr  7445  fzm1  10056  frec2uzltd  10359  0tonninf  10395  sum0  11351  fsumsplit  11370  sumsplitdc  11395  fsum2dlemstep  11397  prod0  11548  fprod2dlemstep  11585  ennnfonelem1  12362  0g0  12630  0ntop  12799  0met  13178  lgsdir2lem3  13725  if0ab  13840  bdcnul  13900  bj-nnelirr  13988