Theorem noel 3878

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 3694	. . 3 ⊢ (𝐴 ∈ (V ∖ V) → 𝐴 ∈ V)
2		eldifn 3695	. . 3 ⊢ (𝐴 ∈ (V ∖ V) → ¬ 𝐴 ∈ V)
3	1, 2	pm2.65i 184	. 2 ⊢ ¬ 𝐴 ∈ (V ∖ V)
4		df-nul 3875	. . 3 ⊢ ∅ = (V ∖ V)
5	4	eleq2i 2680	. 2 ⊢ (𝐴 ∈ ∅ ↔ 𝐴 ∈ (V ∖ V))
6	3, 5	mtbir 312	1 ⊢ ¬ 𝐴 ∈ ∅

Syntax hints:  ¬ wn 3   ∈ wcel 1977  Vcvv 3173   ∖ cdif 3537  ∅c0 3874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543  df-nul 3875

This theorem is referenced by:  n0i  3879  eq0f  3884  n0fOLD  3887  rex0  3894  rab0  3909  rab0OLD  3910  un0  3919  in0  3920  0ss  3924  sbcel12  3935  sbcel2  3941  disj  3969  r19.2zb  4013  ral0  4028  rabsnifsb  4201  int0OLD  4426  iun0  4512  0iun  4513  br0  4631  0xp  5122  csbxp  5123  dm0  5260  dm0rn0  5263  reldm0  5264  elimasni  5411  cnv0OLD  5455  co02  5566  ord0eln0  5696  nlim0  5700  nsuceq0  5722  dffv3  6099  0fv  6137  elfv2ex  6139  mpt20  6623  el2mpt2csbcl  7137  bropopvvv  7142  bropfvvvv  7144  tz7.44-2  7390  omordi  7533  omeulem1  7549  nnmordi  7598  omabs  7614  omsmolem  7620  0er  7667  0erOLD  7668  omxpenlem  7946  en3lp  8396  cantnfle  8451  r1sdom  8520  r1pwss  8530  alephordi  8780  axdc3lem2  9156  zorn2lem7  9207  nlt1pi  9607  xrinf0  12039  elixx3g  12059  elfz2  12204  fzm1  12289  om2uzlti  12611  hashf1lem2  13097  sum0  14299  fsumsplit  14318  sumsplit  14341  fsum2dlem  14343  prod0  14512  fprod2dlem  14549  sadc0  15014  sadcp1  15015  saddisjlem  15024  smu01lem  15045  smu01  15046  smu02  15047  lcmf0  15185  prmreclem5  15462  vdwap0  15518  ram0  15564  0catg  16171  oduclatb  16967  0g0  17086  dfgrp2e  17271  cntzrcl  17583  pmtrfrn  17701  psgnunilem5  17737  gexdvds  17822  gsumzsplit  18150  dprdcntz2  18260  00lss  18763  mplcoe1  19286  mplcoe5  19289  00ply1bas  19431  dsmmbas2  19900  dsmmfi  19901  maducoeval2  20265  madugsum  20268  0ntop  20535  haust1  20966  hauspwdom  21114  kqcldsat  21346  tsmssplit  21765  ustn0  21834  0met  21981  itg11  23264  itg0  23352  bddmulibl  23411  fsumharmonic  24538  ppiublem2  24728  lgsdir2lem3  24852  nbgra0edg  25961  uvtx01vtx  26020  clwwlknprop  26300  2wlkonot3v  26402  2spthonot3v  26403  rusgra0edg  26482  eupath2lem1  26504  helloworld  26713  topnfbey  26717  isarchi  29067  measvuni  29604  ddemeas  29626  sibf0  29723  signstfvneq0  29975  opelco3  30923  wsuclem  31017  wsuclemOLD  31018  unbdqndv1  31669  bj-projval  32177  bj-df-nul  32208  bj-nuliota  32210  finxp0  32404  poimirlem30  32609  pw2f1ocnv  36622  areaquad  36821  ntrneikb  37412  en3lpVD  38102  iblempty  38857  stoweidlem34  38927  sge00  39269  vonhoire  39563  uvtxa01vtx0  40623  vtxdg0v  40688  0enwwlksnge1  41060  wwlks2onv  41158  rusgr0edg  41176  clwwlks  41187  eupth2lem1  41386