Theorem noel 3427

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 3258	. . 3 ⊢ (𝐴 ∈ (V ∖ V) → 𝐴 ∈ V)
2		eldifn 3259	. . 3 ⊢ (𝐴 ∈ (V ∖ V) → ¬ 𝐴 ∈ V)
3	1, 2	pm2.65i 639	. 2 ⊢ ¬ 𝐴 ∈ (V ∖ V)
4		df-nul 3424	. . 3 ⊢ ∅ = (V ∖ V)
5	4	eleq2i 2244	. 2 ⊢ (𝐴 ∈ ∅ ↔ 𝐴 ∈ (V ∖ V))
6	3, 5	mtbir 671	1 ⊢ ¬ 𝐴 ∈ ∅

Syntax hints:  ¬ wn 3   ∈ wcel 2148  Vcvv 2738   ∖ cdif 3127  ∅c0 3423

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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2740  df-dif 3132  df-nul 3424

This theorem is referenced by:  nel02  3428  n0i  3429  n0rf  3436  rex0  3441  eq0  3442  abvor0dc  3447  rab0  3452  un0  3457  in0  3458  0ss  3462  disj  3472  ral0  3525  int0  3859  iun0  3944  0iun  3945  br0  4052  exmid01  4199  nlim0  4395  nsuceq0g  4419  ordtriexmidlem  4519  ordtriexmidlem2  4520  ordtriexmid  4521  ontriexmidim  4522  ordtri2or2exmidlem  4526  onsucelsucexmidlem  4529  reg2exmidlema  4534  reg3exmidlemwe  4579  nn0eln0  4620  0xp  4707  dm0  4842  dm0rn0  4845  reldm0  4846  cnv0  5033  co02  5143  0fv  5551  acexmidlema  5866  acexmidlemb  5867  acexmidlemab  5869  mpo0  5945  nnsucelsuc  6492  nnsucuniel  6496  nnmordi  6517  nnaordex  6529  0er  6569  fidcenumlemrk  6953  nnnninfeq  7126  elni2  7313  nlt1pig  7340  0npr  7482  fzm1  10100  frec2uzltd  10403  0tonninf  10439  sum0  11396  fsumsplit  11415  sumsplitdc  11440  fsum2dlemstep  11442  prod0  11593  fprod2dlemstep  11630  ennnfonelem1  12408  0g0  12795  0ntop  13510  0met  13887  lgsdir2lem3  14434  if0ab  14560  bdcnul  14620  bj-nnelirr  14708