Theorem noel 3413

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 3244	. . 3 ⊢ (𝐴 ∈ (V ∖ V) → 𝐴 ∈ V)
2		eldifn 3245	. . 3 ⊢ (𝐴 ∈ (V ∖ V) → ¬ 𝐴 ∈ V)
3	1, 2	pm2.65i 629	. 2 ⊢ ¬ 𝐴 ∈ (V ∖ V)
4		df-nul 3410	. . 3 ⊢ ∅ = (V ∖ V)
5	4	eleq2i 2233	. 2 ⊢ (𝐴 ∈ ∅ ↔ 𝐴 ∈ (V ∖ V))
6	3, 5	mtbir 661	1 ⊢ ¬ 𝐴 ∈ ∅

Syntax hints:  ¬ wn 3   ∈ wcel 2136  Vcvv 2726   ∖ cdif 3113  ∅c0 3409

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 604  ax-in2 605  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-v 2728  df-dif 3118  df-nul 3410

This theorem is referenced by:  n0i  3414  n0rf  3421  rex0  3426  eq0  3427  abvor0dc  3432  rab0  3437  un0  3442  in0  3443  0ss  3447  disj  3457  ral0  3510  int0  3838  iun0  3922  0iun  3923  br0  4030  exmid01  4177  nlim0  4372  nsuceq0g  4396  ordtriexmidlem  4496  ordtriexmidlem2  4497  ordtriexmid  4498  ontriexmidim  4499  ordtri2or2exmidlem  4503  onsucelsucexmidlem  4506  reg2exmidlema  4511  reg3exmidlemwe  4556  nn0eln0  4597  0xp  4684  dm0  4818  dm0rn0  4821  reldm0  4822  cnv0  5007  co02  5117  0fv  5521  acexmidlema  5833  acexmidlemb  5834  acexmidlemab  5836  mpo0  5912  nnsucelsuc  6459  nnsucuniel  6463  nnmordi  6484  nnaordex  6495  0er  6535  fidcenumlemrk  6919  nnnninfeq  7092  elni2  7255  nlt1pig  7282  0npr  7424  fzm1  10035  frec2uzltd  10338  0tonninf  10374  sum0  11329  fsumsplit  11348  sumsplitdc  11373  fsum2dlemstep  11375  prod0  11526  fprod2dlemstep  11563  ennnfonelem1  12340  0g0  12607  0ntop  12645  0met  13024  lgsdir2lem3  13571  if0ab  13687  bdcnul  13747  bj-nnelirr  13835