Theorem iunid 5024

Description: An indexed union of singletons recovers the index set. (Contributed by NM, 6-Sep-2005.) (Proof shortened by SN, 15-Jan-2025.)

Assertion

Ref	Expression
iunid	⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = 𝐴

Distinct variable group:   𝑥,𝐴

Proof of Theorem iunid

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-iun 4958	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥}}
2		clel5 3622	. . . 4 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑦 = 𝑥)
3		velsn 4600	. . . . 5 ⊢ (𝑦 ∈ {𝑥} ↔ 𝑦 = 𝑥)
4	3	rexbii 3113	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥} ↔ ∃𝑥 ∈ 𝐴 𝑦 = 𝑥)
5	2, 4	bitr4i 281	. . 3 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥})
6	5	eqabi 2899	. 2 ⊢ 𝐴 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥}}
7	1, 6	eqtr4i 2789	1 ⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = 𝐴

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2147  {cab 2741  ∃wrex 3090  {csn 4588  ∪ ciun 4956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rex 3091  df-v 3456  df-sn 4589  df-iun 4958

This theorem is used by:  iunxpconst  5731  fvn0ssdmfun  7106  abnexg  7802  xpexgALT  8027  uniqs  8832  rankcf  10901  dprd2da  20309  t1ficld  23700  discmp  23771  xkoinjcn  24061  metnrmlem2  25235  ovoliunlem1  25878  i1fima  26054  i1fd  26057  itg1addlem5  26076  rnplynfin  26685  dmdju  33339  fnpreimac  33362  gsumpart  33723  elrspunidl  34082  sibfof  35083  bnj1415  35779  1enumen  35848  cvmlift2lem12  36287  poimirlem30  38836  itg2addnclem2  38858  ftc1anclem6  38884  salexct3  47625  salgensscntex  47627  ctvonmbl  47972  vonct  47976