Theorem noel 3201

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	⊢ ¬ A ∈ ∅

Proof of Theorem noel

Step	Hyp	Ref	Expression
1		eldifi 3039	. . 3 ⊢ (A ∈ (V ∖ V) → A ∈ V)
2		eldifn 3040	. . 3 ⊢ (A ∈ (V ∖ V) → ¬ A ∈ V)
3	1, 2	pm2.65i 555	. 2 ⊢ ¬ A ∈ (V ∖ V)
4		df-nul 3198	. . 3 ⊢ ∅ = (V ∖ V)
5	4	eleq2i 2082	. 2 ⊢ (A ∈ ∅ ↔ A ∈ (V ∖ V))
6	3, 5	mtbir 583	1 ⊢ ¬ A ∈ ∅

Syntax hints:  ¬ wn 3   ∈ wcel 1370  Vcvv 2531   ∖ cdif 2887  ∅c0 3197

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 532  ax-in2 533  ax-io 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000

This theorem depends on definitions:  df-bi 110  df-tru 1229  df-nf 1326  df-sb 1624  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-v 2533  df-dif 2893  df-nul 3198

This theorem is referenced by:  n0i  3202  n0rf  3206  rex0  3211  eq0  3212  abvor0dc  3215  rab0  3219  un0  3224  in0  3225  0ss  3228  disj  3241  ral0  3297  int0  3599  iun0  3683  0iun  3684  nlim0  4076  nsuceq0g  4100  ordtriexmidlem  4188  ordtriexmidlem2  4189  ordtriexmid  4190  onsucelsucexmidlem  4194  nn0eln0  4264  0xp  4343  dm0  4472  dm0rn0  4475  reldm0  4476  cnv0  4650  co02  4757  0fv  5129  acexmidlema  5423  acexmidlemb  5424  acexmidlemab  5426  mpt20  5493  nnsucelsuc  5981  nnmordi  5996  nnaordex  6007  0er  6047  elni2  6168  nlt1pig  6195  0npr  6331  bdcnul  7231  bj-nnelirr  7314