Theorem iunid 5027

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 4960	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥}}
2		clel5 3626	. . . 4 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑦 = 𝑥)
3		velsn 4607	. . . . 5 ⊢ (𝑦 ∈ {𝑥} ↔ 𝑦 = 𝑥)
4	3	rexbii 3114	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥} ↔ ∃𝑥 ∈ 𝐴 𝑦 = 𝑥)
5	2, 4	bitr4i 281	. . 3 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥})
6	5	eqabi 2900	. 2 ⊢ 𝐴 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥}}
7	1, 6	eqtr4i 2791	1 ⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = 𝐴

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2146  {cab 2743  ∃wrex 3091  {csn 4591  ∪ ciun 4958

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rex 3092  df-v 3459  df-sn 4592  df-iun 4960

This theorem is used by:  iunxpconst  5736  fvn0ssdmfun  7073  abnexg  7761  xpexgALT  7984  uniqs  8777  rankcf  10779  dprd2da  20160  t1ficld  23536  discmp  23607  xkoinjcn  23897  metnrmlem2  25071  ovoliunlem1  25714  i1fima  25890  i1fd  25893  itg1addlem5  25912  dmdju  33065  fnpreimac  33088  gsumpart  33449  elrspunidl  33802  sibfof  34797  bnj1415  35493  1enumen  35545  cvmlift2lem12  35845  poimirlem30  38360  itg2addnclem2  38382  ftc1anclem6  38408  salexct3  47116  salgensscntex  47118  ctvonmbl  47463  vonct  47467