Theorem noel 4247

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 2142, ax-11 2158, and ax-12 2175. (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 406	. . . . . . 7 ⊢ ¬ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)
2	1	nex 1802	. . . . . 6 ⊢ ¬ ∃𝑦(𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)
3		df-clab 2777	. . . . . . 7 ⊢ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)} ↔ [𝑥 / 𝑦](𝑦 ∈ V ∧ ¬ 𝑦 ∈ V))
4		spsbe 2087	. . . . . . 7 ⊢ ([𝑥 / 𝑦](𝑦 ∈ V ∧ ¬ 𝑦 ∈ V) → ∃𝑦(𝑦 ∈ V ∧ ¬ 𝑦 ∈ V))
5	3, 4	sylbi 220	. . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)} → ∃𝑦(𝑦 ∈ V ∧ ¬ 𝑦 ∈ V))
6	2, 5	mto 200	. . . . 5 ⊢ ¬ 𝑥 ∈ {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)}
7		df-nul 4244	. . . . . . 7 ⊢ ∅ = (V ∖ V)
8		df-dif 3884	. . . . . . 7 ⊢ (V ∖ V) = {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)}
9	7, 8	eqtri 2821	. . . . . 6 ⊢ ∅ = {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)}
10	9	eleq2i 2881	. . . . 5 ⊢ (𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)})
11	6, 10	mtbir 326	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
12	11	intnan 490	. . 3 ⊢ ¬ (𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
13	12	nex 1802	. 2 ⊢ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
14		dfclel 2871	. 2 ⊢ (𝐴 ∈ ∅ ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅))
15	13, 14	mtbir 326	1 ⊢ ¬ 𝐴 ∈ ∅

Syntax hints:  ¬ wn 3   ∧ wa 399   = wceq 1538  ∃wex 1781  [wsb 2069   ∈ wcel 2111  {cab 2776  Vcvv 3441   ∖ cdif 3878  ∅c0 4243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-dif 3884  df-nul 4244

This theorem is referenced by:  nel02  4248  n0i  4249  eq0f  4255  eq0  4258  rex0  4271  rab0  4291  un0  4298  in0  4299  0ss  4304  sbcel12  4316  sbcel2  4323  disj  4355  disjOLD  4356  r19.2zb  4399  ral0  4414  rabsnifsb  4618  iun0  4948  br0  5079  0xp  5613  csbxp  5614  dm0  5754  dm0rn0  5759  reldm0  5762  elimasni  5923  co02  6080  ord0eln0  6213  nlim0  6217  nsuceq0  6239  dffv3  6641  0fv  6684  elfv2ex  6686  mpo0  7218  el2mpocsbcl  7763  bropopvvv  7768  bropfvvvv  7770  tz7.44-2  8026  omordi  8175  nnmordi  8240  omabs  8257  omsmolem  8263  0er  8309  omxpenlem  8601  en3lp  9061  cantnfle  9118  r1sdom  9187  r1pwss  9197  alephordi  9485  axdc3lem2  9862  zorn2lem7  9913  nlt1pi  10317  xrinf0  12719  elixx3g  12739  elfz2  12892  fzm1  12982  om2uzlti  13313  hashf1lem2  13810  sum0  15070  fsumsplit  15089  sumsplit  15115  fsum2dlem  15117  prod0  15289  fprod2dlem  15326  sadc0  15793  sadcp1  15794  saddisjlem  15803  smu01lem  15824  smu01  15825  smu02  15826  lcmf0  15968  prmreclem5  16246  vdwap0  16302  ram0  16348  0catg  16950  oduclatb  17746  0g0  17866  dfgrp2e  18121  cntzrcl  18449  pmtrfrn  18578  psgnunilem5  18614  gexdvds  18701  gsumzsplit  19040  dprdcntz2  19153  00lss  19706  dsmmfi  20427  mplcoe1  20705  mplcoe5  20708  00ply1bas  20869  maducoeval2  21245  madugsum  21248  0ntop  21510  haust1  21957  hauspwdom  22106  kqcldsat  22338  tsmssplit  22757  ustn0  22826  0met  22973  itg11  24295  itg0  24383  bddmulibl  24442  fsumharmonic  25597  ppiublem2  25787  lgsdir2lem3  25911  uvtx01vtx  27187  vtxdg0v  27263  0enwwlksnge1  27650  rusgr0edg  27759  clwwlk  27768  eupth2lem1  28003  helloworld  28250  topnfbey  28254  n0lpligALT  28267  ccatf1  30651  isarchi  30861  measvuni  31583  ddemeas  31605  sibf0  31702  signstfvneq0  31952  opelco3  33131  wsuclem  33225  unbdqndv1  33960  bj-projval  34432  bj-df-nul  34472  bj-nuliota  34474  bj-0nmoore  34527  nlpineqsn  34825  poimirlem30  35087  pw2f1ocnv  39978  areaquad  40166  eu0  40228  ntrneikb  40797  r1rankcld  40939  en3lpVD  41551  supminfxr  42103  liminf0  42435  iblempty  42607  stoweidlem34  42676  sge00  43015  vonhoire  43311  prprelprb  44034  fpprbasnn  44247