Theorem noel 4050

Description: The empty set has no elements. Theorem 6.14 of [Quine] p. 44. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Mario Carneiro, 1-Sep-2015.)

Assertion

Ref	Expression
noel	⊢ ¬ 𝐴 ∈ ∅

Proof of Theorem noel

Step	Hyp	Ref	Expression
1		eldifi 3863	. . 3 ⊢ (𝐴 ∈ (V ∖ V) → 𝐴 ∈ V)
2		eldifn 3864	. . 3 ⊢ (𝐴 ∈ (V ∖ V) → ¬ 𝐴 ∈ V)
3	1, 2	pm2.65i 185	. 2 ⊢ ¬ 𝐴 ∈ (V ∖ V)
4		df-nul 4047	. . 3 ⊢ ∅ = (V ∖ V)
5	4	eleq2i 2819	. 2 ⊢ (𝐴 ∈ ∅ ↔ 𝐴 ∈ (V ∖ V))
6	3, 5	mtbir 312	1 ⊢ ¬ 𝐴 ∈ ∅

Syntax hints:  ¬ wn 3   ∈ wcel 2127  Vcvv 3328   ∖ cdif 3700  ∅c0 4046

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-v 3330  df-dif 3706  df-nul 4047

This theorem is referenced by:  n0i  4051  eq0f  4056  n0fOLD  4059  rex0  4069  rab0  4086  rab0OLD  4087  un0  4098  in0  4099  0ss  4103  sbcel12  4114  sbcel2  4120  disj  4148  r19.2zb  4193  ral0  4208  rabsnifsb  4389  int0OLD  4631  iun0  4716  br0  4841  0xp  5344  csbxp  5345  dm0  5482  dm0rn0  5485  reldm0  5486  elimasni  5638  cnv0OLD  5682  co02  5798  ord0eln0  5928  nlim0  5932  nsuceq0  5954  dffv3  6336  0fv  6376  elfv2ex  6378  mpt20  6878  el2mpt2csbcl  7406  bropopvvv  7411  bropfvvvv  7413  tz7.44-2  7660  omordi  7803  omeulem1  7819  nnmordi  7868  omabs  7884  omsmolem  7890  0er  7936  omxpenlem  8214  en3lp  8670  cantnfle  8729  r1sdom  8798  r1pwss  8808  alephordi  9058  axdc3lem2  9436  zorn2lem7  9487  nlt1pi  9891  xrinf0  12332  elixx3g  12352  elfz2  12497  fzm1  12584  om2uzlti  12914  hashf1lem2  13403  sum0  14622  fsumsplit  14641  sumsplit  14669  fsum2dlem  14671  prod0  14843  fprod2dlem  14880  sadc0  15349  sadcp1  15350  saddisjlem  15359  smu01lem  15380  smu01  15381  smu02  15382  lcmf0  15520  prmreclem5  15797  vdwap0  15853  ram0  15899  0catg  16520  oduclatb  17316  0g0  17435  dfgrp2e  17620  cntzrcl  17931  pmtrfrn  18049  psgnunilem5  18085  gexdvds  18170  gsumzsplit  18498  dprdcntz2  18608  00lss  19115  mplcoe1  19638  mplcoe5  19641  00ply1bas  19783  dsmmbas2  20254  dsmmfi  20255  maducoeval2  20619  madugsum  20622  0ntop  20883  haust1  21329  hauspwdom  21477  kqcldsat  21709  tsmssplit  22127  ustn0  22196  0met  22343  itg11  23628  itg0  23716  bddmulibl  23775  fsumharmonic  24908  ppiublem2  25098  lgsdir2lem3  25222  uvtx01vtx  26471  uvtxa01vtx0OLD  26473  vtxdg0v  26550  0enwwlksnge1  26944  rusgr0edg  27066  clwwlk  27077  eupth2lem1  27341  helloworld  27603  topnfbey  27607  n0lpligALT  27618  isarchi  30016  measvuni  30557  ddemeas  30579  sibf0  30676  signstfvneq0  30929  opelco3  31954  wsuclem  32047  unbdqndv1  32776  bj-projval  33261  bj-df-nul  33294  bj-nuliota  33296  bj-0nmoore  33344  poimirlem30  33721  nel02  34390  pw2f1ocnv  38075  areaquad  38273  ntrneikb  38863  en3lpVD  39548  supminfxr  40161  liminf0  40497  iblempty  40653  stoweidlem34  40723  sge00  41065  vonhoire  41361