Theorem noel 3454

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

Syntax hints:  ¬ wn 3   ∈ wcel 2167  Vcvv 2763   ∖ cdif 3154  ∅c0 3450

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-dif 3159  df-nul 3451

This theorem is referenced by:  nel02  3455  n0i  3456  n0rf  3463  rex0  3468  eq0  3469  abvor0dc  3474  rab0  3479  un0  3484  in0  3485  0ss  3489  disj  3499  ral0  3552  int0  3888  iun0  3973  0iun  3974  br0  4081  exmid01  4231  nlim0  4429  nsuceq0g  4453  ordtriexmidlem  4555  ordtriexmidlem2  4556  ordtriexmid  4557  ontriexmidim  4558  ordtri2or2exmidlem  4562  onsucelsucexmidlem  4565  reg2exmidlema  4570  reg3exmidlemwe  4615  nn0eln0  4656  0xp  4743  dm0  4880  dm0rn0  4883  reldm0  4884  cnv0  5073  co02  5183  0fv  5594  acexmidlema  5913  acexmidlemb  5914  acexmidlemab  5916  mpo0  5992  nnsucelsuc  6549  nnsucuniel  6553  nnmordi  6574  nnaordex  6586  0er  6626  fidcenumlemrk  7020  nnnninfeq  7194  elni2  7381  nlt1pig  7408  0npr  7550  fzm1  10175  frec2uzltd  10495  0tonninf  10532  sum0  11553  fsumsplit  11572  sumsplitdc  11597  fsum2dlemstep  11599  prod0  11750  fprod2dlemstep  11787  ennnfonelem1  12624  0g0  13019  0ntop  14243  0met  14620  lgsdir2lem3  15271  if0ab  15451  bdcnul  15511  bj-nnelirr  15599