Theorem noel 3919

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

Syntax hints:  ¬ wn 3   ∈ wcel 1990  Vcvv 3200   ∖ cdif 3571  ∅c0 3915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-nul 3916

This theorem is referenced by:  n0i  3920  eq0f  3925  n0fOLD  3928  rex0  3938  rab0  3955  rab0OLD  3956  un0  3967  in0  3968  0ss  3972  sbcel12  3983  sbcel2  3989  disj  4017  r19.2zb  4061  ral0  4076  rabsnifsb  4257  int0OLD  4491  iun0  4576  br0  4701  0xp  5199  csbxp  5200  dm0  5339  dm0rn0  5342  reldm0  5343  elimasni  5492  cnv0OLD  5536  co02  5649  ord0eln0  5779  nlim0  5783  nsuceq0  5805  dffv3  6187  0fv  6227  elfv2ex  6229  mpt20  6725  el2mpt2csbcl  7250  bropopvvv  7255  bropfvvvv  7257  tz7.44-2  7503  omordi  7646  omeulem1  7662  nnmordi  7711  omabs  7727  omsmolem  7733  0er  7780  0erOLD  7781  omxpenlem  8061  en3lp  8513  cantnfle  8568  r1sdom  8637  r1pwss  8647  alephordi  8897  axdc3lem2  9273  zorn2lem7  9324  nlt1pi  9728  xrinf0  12168  elixx3g  12188  elfz2  12333  fzm1  12420  om2uzlti  12749  hashf1lem2  13240  sum0  14452  fsumsplit  14471  sumsplit  14499  fsum2dlem  14501  prod0  14673  fprod2dlem  14710  sadc0  15176  sadcp1  15177  saddisjlem  15186  smu01lem  15207  smu01  15208  smu02  15209  lcmf0  15347  prmreclem5  15624  vdwap0  15680  ram0  15726  0catg  16348  oduclatb  17144  0g0  17263  dfgrp2e  17448  cntzrcl  17760  pmtrfrn  17878  psgnunilem5  17914  gexdvds  17999  gsumzsplit  18327  dprdcntz2  18437  00lss  18942  mplcoe1  19465  mplcoe5  19468  00ply1bas  19610  dsmmbas2  20081  dsmmfi  20082  maducoeval2  20446  madugsum  20449  0ntop  20710  haust1  21156  hauspwdom  21304  kqcldsat  21536  tsmssplit  21955  ustn0  22024  0met  22171  itg11  23458  itg0  23546  bddmulibl  23605  fsumharmonic  24738  ppiublem2  24928  lgsdir2lem3  25052  uvtxa01vtx0  26297  vtxdg0v  26369  0enwwlksnge1  26749  wwlks2onv  26847  rusgr0edg  26868  clwwlks  26879  eupth2lem1  27078  helloworld  27321  topnfbey  27325  n0lpligALT  27336  isarchi  29736  measvuni  30277  ddemeas  30299  sibf0  30396  signstfvneq0  30649  opelco3  31678  wsuclem  31773  wsuclemOLD  31774  unbdqndv1  32499  bj-projval  32984  bj-df-nul  33017  bj-nuliota  33019  bj-0nmoore  33067  poimirlem30  33439  nel02  34097  pw2f1ocnv  37604  areaquad  37802  ntrneikb  38392  en3lpVD  39080  supminfxr  39694  liminf0  40025  iblempty  40181  stoweidlem34  40251  sge00  40593  vonhoire  40886