Theorem noel 4296

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.) Remove dependency on ax-10 2145, ax-11 2161, and ax-12 2177. (Revised by Steven Nguyen, 3-May-2023.)

Assertion

Ref	Expression
noel	⊢ ¬ 𝐴 ∈ ∅

Proof of Theorem noel

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		pm3.24 405	. . . . . . 7 ⊢ ¬ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)
2	1	nex 1801	. . . . . 6 ⊢ ¬ ∃𝑦(𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)
3		df-clab 2800	. . . . . . 7 ⊢ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)} ↔ [𝑥 / 𝑦](𝑦 ∈ V ∧ ¬ 𝑦 ∈ V))
4		spsbe 2088	. . . . . . 7 ⊢ ([𝑥 / 𝑦](𝑦 ∈ V ∧ ¬ 𝑦 ∈ V) → ∃𝑦(𝑦 ∈ V ∧ ¬ 𝑦 ∈ V))
5	3, 4	sylbi 219	. . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)} → ∃𝑦(𝑦 ∈ V ∧ ¬ 𝑦 ∈ V))
6	2, 5	mto 199	. . . . 5 ⊢ ¬ 𝑥 ∈ {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)}
7		df-nul 4292	. . . . . . 7 ⊢ ∅ = (V ∖ V)
8		df-dif 3939	. . . . . . 7 ⊢ (V ∖ V) = {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)}
9	7, 8	eqtri 2844	. . . . . 6 ⊢ ∅ = {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)}
10	9	eleq2i 2904	. . . . 5 ⊢ (𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)})
11	6, 10	mtbir 325	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
12	11	intnan 489	. . 3 ⊢ ¬ (𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
13	12	nex 1801	. 2 ⊢ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
14		dfclel 2894	. 2 ⊢ (𝐴 ∈ ∅ ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅))
15	13, 14	mtbir 325	1 ⊢ ¬ 𝐴 ∈ ∅

Syntax hints:  ¬ wn 3   ∧ wa 398   = wceq 1537  ∃wex 1780  [wsb 2069   ∈ wcel 2114  {cab 2799  Vcvv 3494   ∖ cdif 3933  ∅c0 4291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-dif 3939  df-nul 4292

This theorem is referenced by:  nel02  4298  n0i  4299  eq0f  4305  rex0  4317  rab0  4337  un0  4344  in0  4345  0ss  4350  sbcel12  4360  sbcel2  4367  disj  4399  r19.2zb  4441  ral0  4456  rabsnifsb  4658  iun0  4985  br0  5115  0xp  5649  csbxp  5650  dm0  5790  dm0rn0  5795  reldm0  5798  elimasni  5956  co02  6113  ord0eln0  6245  nlim0  6249  nsuceq0  6271  dffv3  6666  0fv  6709  elfv2ex  6711  mpo0  7239  el2mpocsbcl  7780  bropopvvv  7785  bropfvvvv  7787  tz7.44-2  8043  omordi  8192  nnmordi  8257  omabs  8274  omsmolem  8280  0er  8326  omxpenlem  8618  en3lp  9077  cantnfle  9134  r1sdom  9203  r1pwss  9213  alephordi  9500  axdc3lem2  9873  zorn2lem7  9924  nlt1pi  10328  xrinf0  12732  elixx3g  12752  elfz2  12900  fzm1  12988  om2uzlti  13319  hashf1lem2  13815  sum0  15078  fsumsplit  15097  sumsplit  15123  fsum2dlem  15125  prod0  15297  fprod2dlem  15334  sadc0  15803  sadcp1  15804  saddisjlem  15813  smu01lem  15834  smu01  15835  smu02  15836  lcmf0  15978  prmreclem5  16256  vdwap0  16312  ram0  16358  0catg  16958  oduclatb  17754  0g0  17874  dfgrp2e  18129  cntzrcl  18457  pmtrfrn  18586  psgnunilem5  18622  gexdvds  18709  gsumzsplit  19047  dprdcntz2  19160  00lss  19713  mplcoe1  20246  mplcoe5  20249  00ply1bas  20408  dsmmfi  20882  maducoeval2  21249  madugsum  21252  0ntop  21513  haust1  21960  hauspwdom  22109  kqcldsat  22341  tsmssplit  22760  ustn0  22829  0met  22976  itg11  24292  itg0  24380  bddmulibl  24439  fsumharmonic  25589  ppiublem2  25779  lgsdir2lem3  25903  uvtx01vtx  27179  vtxdg0v  27255  0enwwlksnge1  27642  rusgr0edg  27752  clwwlk  27761  eupth2lem1  27997  helloworld  28244  topnfbey  28248  n0lpligALT  28261  ccatf1  30625  isarchi  30811  measvuni  31473  ddemeas  31495  sibf0  31592  signstfvneq0  31842  opelco3  33018  wsuclem  33112  unbdqndv1  33847  bj-projval  34311  bj-df-nul  34351  bj-nuliota  34353  bj-0nmoore  34407  nlpineqsn  34692  poimirlem30  34937  pw2f1ocnv  39683  areaquad  39872  eu0  39935  ntrneikb  40493  r1rankcld  40616  en3lpVD  41228  supminfxr  41789  liminf0  42123  iblempty  42299  stoweidlem34  42368  sge00  42707  vonhoire  43003  prprelprb  43728  fpprbasnn  43943