Theorem iunid 5003

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 4935	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥}}
2		clel5 3607	. . . 4 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑦 = 𝑥)
3		velsn 4583	. . . . 5 ⊢ (𝑦 ∈ {𝑥} ↔ 𝑦 = 𝑥)
4	3	rexbii 3084	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥} ↔ ∃𝑥 ∈ 𝐴 𝑦 = 𝑥)
5	2, 4	bitr4i 278	. . 3 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥})
6	5	eqabi 2871	. 2 ⊢ 𝐴 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥}}
7	1, 6	eqtr4i 2762	1 ⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = 𝐴

Syntax hints:   = wceq 1542   ∈ wcel 2114  {cab 2714  ∃wrex 3061  {csn 4567  ∪ ciun 4933

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rex 3062  df-v 3431  df-sn 4568  df-iun 4935

This theorem is referenced by:  iunxpconst  5704  fvn0ssdmfun  7026  abnexg  7710  xpexgALT  7934  uniqs  8720  rankcf  10700  dprd2da  20019  t1ficld  23292  discmp  23363  xkoinjcn  23652  metnrmlem2  24826  ovoliunlem1  25469  i1fima  25645  i1fd  25648  itg1addlem5  25667  dmdju  32720  fnpreimac  32743  gsumpart  33124  elrspunidl  33488  sibfof  34484  bnj1415  35180  cvmlift2lem12  35496  poimirlem30  37971  itg2addnclem2  37993  ftc1anclem6  38019  salexct3  46770  salgensscntex  46772  ctvonmbl  47117  vonct  47121