Theorem iunid 5019

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 4953	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥}}
2		clel5 3619	. . . 4 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑦 = 𝑥)
3		velsn 4600	. . . . 5 ⊢ (𝑦 ∈ {𝑥} ↔ 𝑦 = 𝑥)
4	3	rexbii 3109	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥} ↔ ∃𝑥 ∈ 𝐴 𝑦 = 𝑥)
5	2, 4	bitr4i 281	. . 3 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥})
6	5	eqabi 2895	. 2 ⊢ 𝐴 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥}}
7	1, 6	eqtr4i 2786	1 ⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = 𝐴

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  {cab 2738  ∃wrex 3086  {csn 4584  ∪ ciun 4951

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 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rex 3087  df-v 3452  df-sn 4585  df-iun 4953

This theorem is used by:  iunxpconst  5728  fvn0ssdmfun  7068  abnexg  7756  xpexgALT  7979  uniqs  8776  rankcf  10789  dprd2da  20174  t1ficld  23555  discmp  23626  xkoinjcn  23916  metnrmlem2  25090  ovoliunlem1  25733  i1fima  25909  i1fd  25912  itg1addlem5  25931  rnplynfin  26542  dmdju  33123  fnpreimac  33146  gsumpart  33506  elrspunidl  33859  sibfof  34854  bnj1415  35550  1enumen  35602  cvmlift2lem12  35896  poimirlem30  38402  itg2addnclem2  38424  ftc1anclem6  38450  salexct3  47173  salgensscntex  47175  ctvonmbl  47520  vonct  47524