Theorem noel 3255

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 3094	. . 3 ⊢ (𝐴 ∈ (V ∖ V) → 𝐴 ∈ V)
2		eldifn 3095	. . 3 ⊢ (𝐴 ∈ (V ∖ V) → ¬ 𝐴 ∈ V)
3	1, 2	pm2.65i 600	. 2 ⊢ ¬ 𝐴 ∈ (V ∖ V)
4		df-nul 3252	. . 3 ⊢ ∅ = (V ∖ V)
5	4	eleq2i 2145	. 2 ⊢ (𝐴 ∈ ∅ ↔ 𝐴 ∈ (V ∖ V))
6	3, 5	mtbir 628	1 ⊢ ¬ 𝐴 ∈ ∅

Syntax hints:  ¬ wn 3   ∈ wcel 1433  Vcvv 2601   ∖ cdif 2970  ∅c0 3251

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 576  ax-in2 577  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-v 2603  df-dif 2975  df-nul 3252

This theorem is referenced by:  n0i  3256  n0rf  3260  rex0  3265  eq0  3266  abvor0dc  3269  rab0  3273  un0  3278  in0  3279  0ss  3282  disj  3292  ral0  3342  int0  3650  iun0  3734  0iun  3735  nlim0  4149  nsuceq0g  4173  ordtriexmidlem  4263  ordtriexmidlem2  4264  ordtriexmid  4265  ordtri2or2exmidlem  4269  onsucelsucexmidlem  4272  reg2exmidlema  4277  reg3exmidlemwe  4321  nn0eln0  4359  0xp  4438  dm0  4567  dm0rn0  4570  reldm0  4571  cnv0  4747  co02  4854  0fv  5229  acexmidlema  5523  acexmidlemb  5524  acexmidlemab  5526  mpt20  5594  nnsucelsuc  6093  nnmordi  6112  nnaordex  6123  0er  6163  elni2  6504  nlt1pig  6531  0npr  6673  fzm1  9117  frec2uzltd  9405  bdcnul  10656  bj-nnelirr  10748