Theorem iunid 5018

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 4951	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥}}
2		clel5 3624	. . . 4 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑦 = 𝑥)
3		velsn 4598	. . . . 5 ⊢ (𝑦 ∈ {𝑥} ↔ 𝑦 = 𝑥)
4	3	rexbii 3109	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥} ↔ ∃𝑥 ∈ 𝐴 𝑦 = 𝑥)
5	2, 4	bitr4i 280	. . 3 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥})
6	5	eqabi 2897	. 2 ⊢ 𝐴 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥}}
7	1, 6	eqtr4i 2788	1 ⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = 𝐴

Syntax hints:   = wceq 1560   ∈ wcel 2142  {cab 2740  ∃wrex 3086  {csn 4582  ∪ ciun 4949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rex 3087  df-v 3456  df-sn 4583  df-iun 4951

This theorem is referenced by:  iunxpconst  5720  fvn0ssdmfun  7055  abnexg  7739  xpexgALT  7962  uniqs  8755  rankcf  10735  dprd2da  20084  t1ficld  23387  discmp  23458  xkoinjcn  23747  metnrmlem2  24921  ovoliunlem1  25564  i1fima  25740  i1fd  25743  itg1addlem5  25762  dmdju  32849  fnpreimac  32872  gsumpart  33243  elrspunidl  33614  sibfof  34637  bnj1415  35333  cvmlift2lem12  35664  poimirlem30  38149  itg2addnclem2  38171  ftc1anclem6  38197  salexct3  46916  salgensscntex  46918  ctvonmbl  47263  vonct  47267