Theorem noel 3495

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 3326	. . 3 ⊢ (𝐴 ∈ (V ∖ V) → 𝐴 ∈ V)
2		eldifn 3327	. . 3 ⊢ (𝐴 ∈ (V ∖ V) → ¬ 𝐴 ∈ V)
3	1, 2	pm2.65i 642	. 2 ⊢ ¬ 𝐴 ∈ (V ∖ V)
4		df-nul 3492	. . 3 ⊢ ∅ = (V ∖ V)
5	4	eleq2i 2296	. 2 ⊢ (𝐴 ∈ ∅ ↔ 𝐴 ∈ (V ∖ V))
6	3, 5	mtbir 675	1 ⊢ ¬ 𝐴 ∈ ∅

Syntax hints:  ¬ wn 3   ∈ wcel 2200  Vcvv 2799   ∖ cdif 3194  ∅c0 3491

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-dif 3199  df-nul 3492

This theorem is referenced by:  nel02  3496  n0i  3497  n0rf  3504  rex0  3509  eq0  3510  abvor0dc  3515  rab0  3520  un0  3525  in0  3526  0ss  3530  disj  3540  ral0  3593  int0  3937  iun0  4022  0iun  4023  br0  4132  exmid01  4282  nlim0  4485  nsuceq0g  4509  ordtriexmidlem  4611  ordtriexmidlem2  4612  ordtriexmid  4613  ontriexmidim  4614  ordtri2or2exmidlem  4618  onsucelsucexmidlem  4621  reg2exmidlema  4626  reg3exmidlemwe  4671  nn0eln0  4712  0xp  4799  dm0  4937  dm0rn0  4940  reldm0  4941  cnv0  5132  co02  5242  0fv  5667  acexmidlema  5998  acexmidlemb  5999  acexmidlemab  6001  mpo0  6080  nnsucelsuc  6645  nnsucuniel  6649  nnmordi  6670  nnaordex  6682  0er  6722  elssdc  7075  fidcenumlemrk  7132  nnnninfeq  7306  iftrueb01  7419  pw1if  7421  elni2  7512  nlt1pig  7539  0npr  7681  fzm1  10308  frec2uzltd  10637  0tonninf  10674  sum0  11914  fsumsplit  11933  sumsplitdc  11958  fsum2dlemstep  11960  prod0  12111  fprod2dlemstep  12148  ennnfonelem1  12993  0g0  13424  0ntop  14696  0met  15073  lgsdir2lem3  15724  vtxdg0v  16053  if0ab  16224  bdcnul  16283  bj-nnelirr  16371  nnnninfex  16448