Theorem noel 3495

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

Syntax hints:  ¬ wn 3   ∈ wcel 2200  Vcvv 2799   ∖ cdif 3194  ∅c0 3491

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 2801  df-dif 3199  df-nul 3492

This theorem is referenced by:  nel02  3496  n0i  3497  n0rf  3504  rex0  3509  eq0  3510  abvor0dc  3515  rab0  3520  un0  3525  in0  3526  0ss  3530  disj  3540  ral0  3593  int0  3936  iun0  4021  0iun  4022  br0  4131  exmid01  4281  nlim0  4484  nsuceq0g  4508  ordtriexmidlem  4610  ordtriexmidlem2  4611  ordtriexmid  4612  ontriexmidim  4613  ordtri2or2exmidlem  4617  onsucelsucexmidlem  4620  reg2exmidlema  4625  reg3exmidlemwe  4670  nn0eln0  4711  0xp  4798  dm0  4936  dm0rn0  4939  reldm0  4940  cnv0  5131  co02  5241  0fv  5664  acexmidlema  5991  acexmidlemb  5992  acexmidlemab  5994  mpo0  6073  nnsucelsuc  6635  nnsucuniel  6639  nnmordi  6660  nnaordex  6672  0er  6712  fidcenumlemrk  7117  nnnninfeq  7291  iftrueb01  7404  pw1if  7406  elni2  7497  nlt1pig  7524  0npr  7666  fzm1  10292  frec2uzltd  10620  0tonninf  10657  sum0  11894  fsumsplit  11913  sumsplitdc  11938  fsum2dlemstep  11940  prod0  12091  fprod2dlemstep  12128  ennnfonelem1  12973  0g0  13404  0ntop  14675  0met  15052  lgsdir2lem3  15703  if0ab  16127  bdcnul  16186  bj-nnelirr  16274  nnnninfex  16347