Theorem noel 4185

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 2079, ax-11 2093, and ax-12 2106. (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 394	. . . . . . 7 ⊢ ¬ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)
2	1	nex 1763	. . . . . 6 ⊢ ¬ ∃𝑦(𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)
3		df-clab 2759	. . . . . . 7 ⊢ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)} ↔ [𝑥 / 𝑦](𝑦 ∈ V ∧ ¬ 𝑦 ∈ V))
4		spsbe 2033	. . . . . . 7 ⊢ ([𝑥 / 𝑦](𝑦 ∈ V ∧ ¬ 𝑦 ∈ V) → ∃𝑦(𝑦 ∈ V ∧ ¬ 𝑦 ∈ V))
5	3, 4	sylbi 209	. . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)} → ∃𝑦(𝑦 ∈ V ∧ ¬ 𝑦 ∈ V))
6	2, 5	mto 189	. . . . 5 ⊢ ¬ 𝑥 ∈ {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)}
7		df-nul 4181	. . . . . . 7 ⊢ ∅ = (V ∖ V)
8		df-dif 3834	. . . . . . 7 ⊢ (V ∖ V) = {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)}
9	7, 8	eqtri 2802	. . . . . 6 ⊢ ∅ = {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)}
10	9	eleq2i 2857	. . . . 5 ⊢ (𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)})
11	6, 10	mtbir 315	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
12	11	intnan 479	. . 3 ⊢ ¬ (𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
13	12	nex 1763	. 2 ⊢ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
14		dfclel 2847	. 2 ⊢ (𝐴 ∈ ∅ ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅))
15	13, 14	mtbir 315	1 ⊢ ¬ 𝐴 ∈ ∅

Syntax hints:  ¬ wn 3   ∧ wa 387   = wceq 1507  ∃wex 1742  [wsb 2015   ∈ wcel 2050  {cab 2758  Vcvv 3415   ∖ cdif 3828  ∅c0 4180

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-ext 2750

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-dif 3834  df-nul 4181

This theorem is referenced by:  n0i  4187  eq0f  4193  rex0  4205  rab0  4225  un0  4232  in0  4233  0ss  4237  sbcel12  4247  sbcel2  4254  disj  4283  r19.2zb  4325  ral0  4340  rabsnifsb  4533  iun0  4852  br0  4979  0xp  5500  csbxp  5501  dm0  5638  dm0rn0  5641  reldm0  5642  elimasni  5798  co02  5954  ord0eln0  6085  nlim0  6089  nsuceq0  6111  dffv3  6497  0fv  6541  elfv2ex  6543  mpo0  7057  el2mpocsbcl  7590  bropopvvv  7595  bropfvvvv  7597  tz7.44-2  7849  omordi  7995  nnmordi  8060  omabs  8076  omsmolem  8082  0er  8128  omxpenlem  8416  en3lp  8873  cantnfle  8930  r1sdom  8999  r1pwss  9009  alephordi  9296  axdc3lem2  9673  zorn2lem7  9724  nlt1pi  10128  xrinf0  12550  elixx3g  12570  elfz2  12718  fzm1  12806  om2uzlti  13136  hashf1lem2  13630  sum0  14941  fsumsplit  14960  sumsplit  14986  fsum2dlem  14988  prod0  15160  fprod2dlem  15197  sadc0  15666  sadcp1  15667  saddisjlem  15676  smu01lem  15697  smu01  15698  smu02  15699  lcmf0  15837  prmreclem5  16115  vdwap0  16171  ram0  16217  0catg  16819  oduclatb  17615  0g0  17734  dfgrp2e  17920  cntzrcl  18231  pmtrfrn  18350  psgnunilem5  18386  psgnunilem5OLD  18387  gexdvds  18473  gsumzsplit  18803  dprdcntz2  18913  00lss  19438  mplcoe1  19962  mplcoe5  19965  00ply1bas  20114  dsmmbas2  20586  dsmmfi  20587  maducoeval2  20956  madugsum  20959  0ntop  21220  haust1  21667  hauspwdom  21816  kqcldsat  22048  tsmssplit  22466  ustn0  22535  0met  22682  itg11  23998  itg0  24086  bddmulibl  24145  fsumharmonic  25294  ppiublem2  25484  lgsdir2lem3  25608  uvtx01vtx  26885  vtxdg0v  26961  0enwwlksnge1  27353  rusgr0edg  27482  clwwlk  27492  eupth2lem1  27751  helloworld  28024  topnfbey  28028  n0lpligALT  28041  isarchi  30477  measvuni  31118  ddemeas  31140  sibf0  31237  signstfvneq0  31489  opelco3  32538  wsuclem  32633  unbdqndv1  33367  bj-projval  33826  bj-df-nul  33859  bj-nuliota  33861  bj-0nmoore  33915  nlpineqsn  34130  poimirlem30  34363  nel02  35027  pw2f1ocnv  39030  areaquad  39219  ntrneikb  39807  r1rankcld  39942  en3lpVD  40598  supminfxr  41172  liminf0  41506  iblempty  41681  stoweidlem34  41751  sge00  42090  vonhoire  42386  prprelprb  43048  fpprbasnn  43263