Theorem noel 3468

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 3299	. . 3 ⊢ (𝐴 ∈ (V ∖ V) → 𝐴 ∈ V)
2		eldifn 3300	. . 3 ⊢ (𝐴 ∈ (V ∖ V) → ¬ 𝐴 ∈ V)
3	1, 2	pm2.65i 640	. 2 ⊢ ¬ 𝐴 ∈ (V ∖ V)
4		df-nul 3465	. . 3 ⊢ ∅ = (V ∖ V)
5	4	eleq2i 2273	. 2 ⊢ (𝐴 ∈ ∅ ↔ 𝐴 ∈ (V ∖ V))
6	3, 5	mtbir 673	1 ⊢ ¬ 𝐴 ∈ ∅

Syntax hints:  ¬ wn 3   ∈ wcel 2177  Vcvv 2773   ∖ cdif 3167  ∅c0 3464

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-dif 3172  df-nul 3465

This theorem is referenced by:  nel02  3469  n0i  3470  n0rf  3477  rex0  3482  eq0  3483  abvor0dc  3488  rab0  3493  un0  3498  in0  3499  0ss  3503  disj  3513  ral0  3566  int0  3905  iun0  3990  0iun  3991  br0  4100  exmid01  4250  nlim0  4449  nsuceq0g  4473  ordtriexmidlem  4575  ordtriexmidlem2  4576  ordtriexmid  4577  ontriexmidim  4578  ordtri2or2exmidlem  4582  onsucelsucexmidlem  4585  reg2exmidlema  4590  reg3exmidlemwe  4635  nn0eln0  4676  0xp  4763  dm0  4901  dm0rn0  4904  reldm0  4905  cnv0  5095  co02  5205  0fv  5625  acexmidlema  5948  acexmidlemb  5949  acexmidlemab  5951  mpo0  6028  nnsucelsuc  6590  nnsucuniel  6594  nnmordi  6615  nnaordex  6627  0er  6667  fidcenumlemrk  7071  nnnninfeq  7245  iftrueb01  7354  pw1if  7356  elni2  7447  nlt1pig  7474  0npr  7616  fzm1  10242  frec2uzltd  10570  0tonninf  10607  sum0  11774  fsumsplit  11793  sumsplitdc  11818  fsum2dlemstep  11820  prod0  11971  fprod2dlemstep  12008  ennnfonelem1  12853  0g0  13283  0ntop  14554  0met  14931  lgsdir2lem3  15582  if0ab  15880  bdcnul  15939  bj-nnelirr  16027  nnnninfex  16100