Theorem noel 4120

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 3931	. . 3 ⊢ (𝐴 ∈ (V ∖ V) → 𝐴 ∈ V)
2		eldifn 3932	. . 3 ⊢ (𝐴 ∈ (V ∖ V) → ¬ 𝐴 ∈ V)
3	1, 2	pm2.65i 185	. 2 ⊢ ¬ 𝐴 ∈ (V ∖ V)
4		df-nul 4117	. . 3 ⊢ ∅ = (V ∖ V)
5	4	eleq2i 2877	. 2 ⊢ (𝐴 ∈ ∅ ↔ 𝐴 ∈ (V ∖ V))
6	3, 5	mtbir 314	1 ⊢ ¬ 𝐴 ∈ ∅

Syntax hints:  ¬ wn 3   ∈ wcel 2156  Vcvv 3391   ∖ cdif 3766  ∅c0 4116

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-v 3393  df-dif 3772  df-nul 4117

This theorem is referenced by:  n0i  4121  eq0f  4127  rex0  4139  rab0  4156  un0  4165  in0  4166  0ss  4170  sbcel12  4180  sbcel2  4186  disj  4214  r19.2zb  4256  ral0  4271  rabsnifsb  4448  iun0  4768  br0  4893  0xp  5401  csbxp  5402  dm0  5540  dm0rn0  5543  reldm0  5544  elimasni  5702  cnv0OLD  5747  co02  5863  ord0eln0  5991  nlim0  5995  nsuceq0  6017  dffv3  6400  0fv  6443  elfv2ex  6445  mpt20  6951  el2mpt2csbcl  7479  bropopvvv  7485  bropfvvvv  7487  tz7.44-2  7735  omordi  7879  omeulem1  7895  nnmordi  7944  omabs  7960  omsmolem  7966  0er  8012  omxpenlem  8296  en3lp  8752  cantnfle  8811  r1sdom  8880  r1pwss  8890  alephordi  9176  axdc3lem2  9554  zorn2lem7  9605  nlt1pi  10009  xrinf0  12382  elixx3g  12402  elfz2  12552  fzm1  12639  om2uzlti  12969  hashf1lem2  13453  sum0  14671  fsumsplit  14690  sumsplit  14718  fsum2dlem  14720  prod0  14890  fprod2dlem  14927  sadc0  15391  sadcp1  15392  saddisjlem  15401  smu01lem  15422  smu01  15423  smu02  15424  lcmf0  15562  prmreclem5  15837  vdwap0  15893  ram0  15939  0catg  16548  oduclatb  17345  0g0  17464  dfgrp2e  17649  cntzrcl  17957  pmtrfrn  18075  psgnunilem5  18111  gexdvds  18196  gsumzsplit  18524  dprdcntz2  18635  00lss  19142  mplcoe1  19670  mplcoe5  19673  00ply1bas  19814  dsmmbas2  20287  dsmmfi  20288  maducoeval2  20653  madugsum  20656  0ntop  20919  haust1  21366  hauspwdom  21514  kqcldsat  21746  tsmssplit  22164  ustn0  22233  0met  22380  itg11  23668  itg0  23756  bddmulibl  23815  fsumharmonic  24948  ppiublem2  25138  lgsdir2lem3  25262  uvtx01vtx  26514  uvtxa01vtx0OLD  26516  vtxdg0v  26593  0enwwlksnge1  26987  rusgr0edg  27111  clwwlk  27122  eupth2lem1  27387  helloworld  27648  topnfbey  27652  n0lpligALT  27663  isarchi  30057  measvuni  30598  ddemeas  30620  sibf0  30717  signstfvneq0  30970  opelco3  31993  wsuclem  32086  unbdqndv1  32811  bj-projval  33289  bj-df-nul  33322  bj-nuliota  33324  bj-0nmoore  33373  poimirlem30  33747  nel02  34407  pw2f1ocnv  38099  areaquad  38296  ntrneikb  38886  en3lpVD  39568  supminfxr  40167  liminf0  40499  iblempty  40654  stoweidlem34  40724  sge00  41066  vonhoire  41362