Theorem noel 3450

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

Syntax hints:  ¬ wn 3   ∈ wcel 2164  Vcvv 2760   ∖ cdif 3150  ∅c0 3446

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-dif 3155  df-nul 3447

This theorem is referenced by:  nel02  3451  n0i  3452  n0rf  3459  rex0  3464  eq0  3465  abvor0dc  3470  rab0  3475  un0  3480  in0  3481  0ss  3485  disj  3495  ral0  3548  int0  3884  iun0  3969  0iun  3970  br0  4077  exmid01  4227  nlim0  4425  nsuceq0g  4449  ordtriexmidlem  4551  ordtriexmidlem2  4552  ordtriexmid  4553  ontriexmidim  4554  ordtri2or2exmidlem  4558  onsucelsucexmidlem  4561  reg2exmidlema  4566  reg3exmidlemwe  4611  nn0eln0  4652  0xp  4739  dm0  4876  dm0rn0  4879  reldm0  4880  cnv0  5069  co02  5179  0fv  5590  acexmidlema  5909  acexmidlemb  5910  acexmidlemab  5912  mpo0  5988  nnsucelsuc  6544  nnsucuniel  6548  nnmordi  6569  nnaordex  6581  0er  6621  fidcenumlemrk  7013  nnnninfeq  7187  elni2  7374  nlt1pig  7401  0npr  7543  fzm1  10166  frec2uzltd  10474  0tonninf  10511  sum0  11531  fsumsplit  11550  sumsplitdc  11575  fsum2dlemstep  11577  prod0  11728  fprod2dlemstep  11765  ennnfonelem1  12564  0g0  12959  0ntop  14175  0met  14552  lgsdir2lem3  15146  if0ab  15297  bdcnul  15357  bj-nnelirr  15445