Theorem noel 4344

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 2139, ax-11 2155, and ax-12 2175. (Revised by Steven Nguyen, 3-May-2023.) (Proof shortened by BJ, 23-Sep-2024.)

Assertion

Ref	Expression
noel	⊢ ¬ 𝐴 ∈ ∅

Proof of Theorem noel

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nsb 2104	. . . . . 6 ⊢ (∀𝑦 ¬ ⊥ → ¬ [𝑥 / 𝑦]⊥)
2		fal 1551	. . . . . 6 ⊢ ¬ ⊥
3	1, 2	mpg 1794	. . . . 5 ⊢ ¬ [𝑥 / 𝑦]⊥
4		dfnul4 4341	. . . . . . 7 ⊢ ∅ = {𝑦 ∣ ⊥}
5	4	eleq2i 2831	. . . . . 6 ⊢ (𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑦 ∣ ⊥})
6		df-clab 2713	. . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥)
7	5, 6	bitri 275	. . . . 5 ⊢ (𝑥 ∈ ∅ ↔ [𝑥 / 𝑦]⊥)
8	3, 7	mtbir 323	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
9	8	intnan 486	. . 3 ⊢ ¬ (𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
10	9	nex 1797	. 2 ⊢ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
11		dfclel 2815	. 2 ⊢ (𝐴 ∈ ∅ ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅))
12	10, 11	mtbir 323	1 ⊢ ¬ 𝐴 ∈ ∅

Syntax hints:  ¬ wn 3   ∧ wa 395   = wceq 1537  ⊥wfal 1549  ∃wex 1776  [wsb 2062   ∈ wcel 2106  {cab 2712  ∅c0 4339

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-dif 3966  df-nul 4340

This theorem is referenced by:  nel02  4345  n0i  4346  eq0f  4353  eq0ALT  4357  rex0  4366  rab0  4392  un0  4400  in0  4401  0ss  4406  sbcel12  4417  sbcel2  4424  disj  4456  r19.2zb  4502  rabsnifsb  4727  iun0  5067  br0  5197  0xp  5787  csbxp  5788  dm0  5934  dm0rn0  5938  reldm0  5941  elimasni  6112  co02  6282  ord0eln0  6441  nlim0  6445  nsuceq0  6469  dffv3  6903  0fv  6951  elfv2ex  6953  mpo0  7518  el2mpocsbcl  8109  bropopvvv  8114  bropfvvvv  8116  tz7.44-2  8446  omordi  8603  nnmordi  8668  omabs  8688  omsmolem  8694  0er  8782  omxpenlem  9112  infn0  9338  en3lp  9652  cantnfle  9709  r1sdom  9812  r1pwss  9822  alephordi  10112  axdc3lem2  10489  zorn2lem7  10540  nlt1pi  10944  xrinf0  13377  elixx3g  13397  elfz2  13551  fzm1  13644  om2uzlti  13988  hashf1lem2  14492  sum0  15754  fsumsplit  15774  sumsplit  15801  fsum2dlem  15803  prod0  15976  fprod2dlem  16013  sadc0  16488  sadcp1  16489  saddisjlem  16498  smu01lem  16519  smu01  16520  smu02  16521  lcmf0  16668  prmreclem5  16954  vdwap0  17010  ram0  17056  0catg  17733  oduclatb  18565  0g0  18690  dfgrp2e  18994  cntzrcl  19358  pmtrfrn  19491  psgnunilem5  19527  gexdvds  19617  gsumzsplit  19960  dprdcntz2  20073  00lss  20957  dsmmfi  21776  mplcoe1  22073  mplcoe5  22076  00ply1bas  22257  maducoeval2  22662  madugsum  22665  0ntop  22927  haust1  23376  hauspwdom  23525  kqcldsat  23757  tsmssplit  24176  ustn0  24245  0met  24392  itg11  25740  itg0  25830  bddmulibl  25889  fsumharmonic  27070  ppiublem2  27262  lgsdir2lem3  27386  nulsslt  27857  nulssgt  27858  uvtx01vtx  29429  vtxdg0v  29506  0enwwlksnge1  29894  rusgr0edg  30003  clwwlk  30012  eupth2lem1  30247  helloworld  30494  topnfbey  30498  n0lpligALT  30513  ccatf1  32918  isarchi  33172  constrmon  33749  measvuni  34195  ddemeas  34217  sibf0  34316  signstfvneq0  34566  opelco3  35756  wsuclem  35807  unbdqndv1  36491  bj-projval  36979  bj-nuliota  37040  bj-0nmoore  37095  nlpineqsn  37391  poimirlem30  37637  pw2f1ocnv  43026  areaquad  43205  onexlimgt  43232  cantnfresb  43314  succlg  43318  oacl2g  43320  omabs2  43322  omcl2  43323  eu0  43510  ntrneikb  44084  r1rankcld  44227  en3lpVD  44843  supminfxr  45414  liminf0  45749  iblempty  45921  stoweidlem34  45990  sge00  46332  vonhoire  46628  prprelprb  47442  fpprbasnn  47654  stgr0  47863