Theorem noel 3463

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 3294	. . 3 ⊢ (𝐴 ∈ (V ∖ V) → 𝐴 ∈ V)
2		eldifn 3295	. . 3 ⊢ (𝐴 ∈ (V ∖ V) → ¬ 𝐴 ∈ V)
3	1, 2	pm2.65i 640	. 2 ⊢ ¬ 𝐴 ∈ (V ∖ V)
4		df-nul 3460	. . 3 ⊢ ∅ = (V ∖ V)
5	4	eleq2i 2271	. 2 ⊢ (𝐴 ∈ ∅ ↔ 𝐴 ∈ (V ∖ V))
6	3, 5	mtbir 672	1 ⊢ ¬ 𝐴 ∈ ∅

Syntax hints:  ¬ wn 3   ∈ wcel 2175  Vcvv 2771   ∖ cdif 3162  ∅c0 3459

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 615  ax-in2 616  ax-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-v 2773  df-dif 3167  df-nul 3460

This theorem is referenced by:  nel02  3464  n0i  3465  n0rf  3472  rex0  3477  eq0  3478  abvor0dc  3483  rab0  3488  un0  3493  in0  3494  0ss  3498  disj  3508  ral0  3561  int0  3898  iun0  3983  0iun  3984  br0  4091  exmid01  4241  nlim0  4440  nsuceq0g  4464  ordtriexmidlem  4566  ordtriexmidlem2  4567  ordtriexmid  4568  ontriexmidim  4569  ordtri2or2exmidlem  4573  onsucelsucexmidlem  4576  reg2exmidlema  4581  reg3exmidlemwe  4626  nn0eln0  4667  0xp  4754  dm0  4891  dm0rn0  4894  reldm0  4895  cnv0  5085  co02  5195  0fv  5611  acexmidlema  5934  acexmidlemb  5935  acexmidlemab  5937  mpo0  6014  nnsucelsuc  6576  nnsucuniel  6580  nnmordi  6601  nnaordex  6613  0er  6653  fidcenumlemrk  7055  nnnninfeq  7229  elni2  7426  nlt1pig  7453  0npr  7595  fzm1  10221  frec2uzltd  10546  0tonninf  10583  sum0  11641  fsumsplit  11660  sumsplitdc  11685  fsum2dlemstep  11687  prod0  11838  fprod2dlemstep  11875  ennnfonelem1  12720  0g0  13150  0ntop  14421  0met  14798  lgsdir2lem3  15449  if0ab  15674  bdcnul  15734  bj-nnelirr  15822  nnnninfex  15892