Theorem iunid 5036

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 4969	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥}}
2		clel5 3644	. . . 4 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑦 = 𝑥)
3		velsn 4617	. . . . 5 ⊢ (𝑦 ∈ {𝑥} ↔ 𝑦 = 𝑥)
4	3	rexbii 3083	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥} ↔ ∃𝑥 ∈ 𝐴 𝑦 = 𝑥)
5	2, 4	bitr4i 278	. . 3 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥})
6	5	eqabi 2870	. 2 ⊢ 𝐴 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥}}
7	1, 6	eqtr4i 2761	1 ⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = 𝐴

Syntax hints:   = wceq 1540   ∈ wcel 2108  {cab 2713  ∃wrex 3060  {csn 4601  ∪ ciun 4967

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rex 3061  df-v 3461  df-sn 4602  df-iun 4969

This theorem is referenced by:  iunxpconst  5727  fvn0ssdmfun  7064  abnexg  7750  xpexgALT  7980  uniqs  8791  rankcf  10791  dprd2da  20025  t1ficld  23265  discmp  23336  xkoinjcn  23625  metnrmlem2  24800  ovoliunlem1  25455  i1fima  25631  i1fd  25634  itg1addlem5  25653  dmdju  32625  fnpreimac  32649  gsumpart  33051  elrspunidl  33443  sibfof  34372  bnj1415  35069  cvmlift2lem12  35336  poimirlem30  37674  itg2addnclem2  37696  ftc1anclem6  37722  uniqsALTV  38347  salexct3  46371  salgensscntex  46373  ctvonmbl  46718  vonct  46722