Theorem noel 3901

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 3716	. . 3 ⊢ (𝐴 ∈ (V ∖ V) → 𝐴 ∈ V)
2		eldifn 3717	. . 3 ⊢ (𝐴 ∈ (V ∖ V) → ¬ 𝐴 ∈ V)
3	1, 2	pm2.65i 185	. 2 ⊢ ¬ 𝐴 ∈ (V ∖ V)
4		df-nul 3898	. . 3 ⊢ ∅ = (V ∖ V)
5	4	eleq2i 2690	. 2 ⊢ (𝐴 ∈ ∅ ↔ 𝐴 ∈ (V ∖ V))
6	3, 5	mtbir 313	1 ⊢ ¬ 𝐴 ∈ ∅

Syntax hints:  ¬ wn 3   ∈ wcel 1987  Vcvv 3190   ∖ cdif 3557  ∅c0 3897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3192  df-dif 3563  df-nul 3898

This theorem is referenced by:  n0i  3902  eq0f  3907  n0fOLD  3910  rex0  3920  rab0  3935  rab0OLD  3936  un0  3945  in0  3946  0ss  3950  sbcel12  3961  sbcel2  3967  disj  3995  r19.2zb  4039  ral0  4054  rabsnifsb  4234  int0OLD  4463  iun0  4549  br0  4671  0xp  5170  csbxp  5171  dm0  5309  dm0rn0  5312  reldm0  5313  elimasni  5461  cnv0OLD  5505  co02  5618  ord0eln0  5748  nlim0  5752  nsuceq0  5774  dffv3  6154  0fv  6194  elfv2ex  6196  mpt20  6690  el2mpt2csbcl  7210  bropopvvv  7215  bropfvvvv  7217  tz7.44-2  7463  omordi  7606  omeulem1  7622  nnmordi  7671  omabs  7687  omsmolem  7693  0er  7740  0erOLD  7741  omxpenlem  8021  en3lp  8473  cantnfle  8528  r1sdom  8597  r1pwss  8607  alephordi  8857  axdc3lem2  9233  zorn2lem7  9284  nlt1pi  9688  xrinf0  12126  elixx3g  12146  elfz2  12291  fzm1  12377  om2uzlti  12705  hashf1lem2  13194  sum0  14401  fsumsplit  14420  sumsplit  14446  fsum2dlem  14448  prod0  14617  fprod2dlem  14654  sadc0  15119  sadcp1  15120  saddisjlem  15129  smu01lem  15150  smu01  15151  smu02  15152  lcmf0  15290  prmreclem5  15567  vdwap0  15623  ram0  15669  0catg  16288  oduclatb  17084  0g0  17203  dfgrp2e  17388  cntzrcl  17700  pmtrfrn  17818  psgnunilem5  17854  gexdvds  17939  gsumzsplit  18267  dprdcntz2  18377  00lss  18882  mplcoe1  19405  mplcoe5  19408  00ply1bas  19550  dsmmbas2  20021  dsmmfi  20022  maducoeval2  20386  madugsum  20389  0ntop  20650  haust1  21096  hauspwdom  21244  kqcldsat  21476  tsmssplit  21895  ustn0  21964  0met  22111  itg11  23398  itg0  23486  bddmulibl  23545  fsumharmonic  24672  ppiublem2  24862  lgsdir2lem3  24986  uvtxa01vtx0  26218  vtxdg0v  26289  0enwwlksnge1  26652  wwlks2onv  26750  rusgr0edg  26769  clwwlks  26780  eupth2lem1  26978  helloworld  27209  topnfbey  27213  n0lpligALT  27224  isarchi  29563  measvuni  30100  ddemeas  30122  sibf0  30219  signstfvneq0  30471  opelco3  31433  wsuclem  31527  wsuclemOLD  31528  unbdqndv1  32194  bj-projval  32684  bj-df-nul  32717  bj-nuliota  32719  poimirlem30  33110  pw2f1ocnv  37123  areaquad  37322  ntrneikb  37913  en3lpVD  38602  iblempty  39518  stoweidlem34  39588  sge00  39930  vonhoire  40223