Theorem noel 3438

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

Syntax hints:  ¬ wn 3   ∈ wcel 2158  Vcvv 2749   ∖ cdif 3138  ∅c0 3434

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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-v 2751  df-dif 3143  df-nul 3435

This theorem is referenced by:  nel02  3439  n0i  3440  n0rf  3447  rex0  3452  eq0  3453  abvor0dc  3458  rab0  3463  un0  3468  in0  3469  0ss  3473  disj  3483  ral0  3536  int0  3870  iun0  3955  0iun  3956  br0  4063  exmid01  4210  nlim0  4406  nsuceq0g  4430  ordtriexmidlem  4530  ordtriexmidlem2  4531  ordtriexmid  4532  ontriexmidim  4533  ordtri2or2exmidlem  4537  onsucelsucexmidlem  4540  reg2exmidlema  4545  reg3exmidlemwe  4590  nn0eln0  4631  0xp  4718  dm0  4853  dm0rn0  4856  reldm0  4857  cnv0  5044  co02  5154  0fv  5562  acexmidlema  5879  acexmidlemb  5880  acexmidlemab  5882  mpo0  5958  nnsucelsuc  6506  nnsucuniel  6510  nnmordi  6531  nnaordex  6543  0er  6583  fidcenumlemrk  6967  nnnninfeq  7140  elni2  7327  nlt1pig  7354  0npr  7496  fzm1  10114  frec2uzltd  10417  0tonninf  10453  sum0  11410  fsumsplit  11429  sumsplitdc  11454  fsum2dlemstep  11456  prod0  11607  fprod2dlemstep  11644  ennnfonelem1  12422  0g0  12814  0ntop  13860  0met  14237  lgsdir2lem3  14784  if0ab  14910  bdcnul  14970  bj-nnelirr  15058