Theorem iunid 4795

Description: An indexed union of singletons recovers the index set. (Contributed by NM, 6-Sep-2005.)

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-sn 4398	. . . . 5 ⊢ {𝑥} = {𝑦 ∣ 𝑦 = 𝑥}
2		equcom 2122	. . . . . 6 ⊢ (𝑦 = 𝑥 ↔ 𝑥 = 𝑦)
3	2	abbii 2944	. . . . 5 ⊢ {𝑦 ∣ 𝑦 = 𝑥} = {𝑦 ∣ 𝑥 = 𝑦}
4	1, 3	eqtri 2849	. . . 4 ⊢ {𝑥} = {𝑦 ∣ 𝑥 = 𝑦}
5	4	a1i 11	. . 3 ⊢ (𝑥 ∈ 𝐴 → {𝑥} = {𝑦 ∣ 𝑥 = 𝑦})
6	5	iuneq2i 4759	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = ∪ 𝑥 ∈ 𝐴 {𝑦 ∣ 𝑥 = 𝑦}
7		iunab 4786	. . 3 ⊢ ∪ 𝑥 ∈ 𝐴 {𝑦 ∣ 𝑥 = 𝑦} = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑥 = 𝑦}
8		risset 3272	. . . 4 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑥 = 𝑦)
9	8	abbii 2944	. . 3 ⊢ {𝑦 ∣ 𝑦 ∈ 𝐴} = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑥 = 𝑦}
10		abid2 2950	. . 3 ⊢ {𝑦 ∣ 𝑦 ∈ 𝐴} = 𝐴
11	7, 9, 10	3eqtr2i 2855	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 {𝑦 ∣ 𝑥 = 𝑦} = 𝐴
12	6, 11	eqtri 2849	1 ⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = 𝐴

Syntax hints:   = wceq 1656   ∈ wcel 2164  {cab 2811  ∃wrex 3118  {csn 4397  ∪ ciun 4740

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ral 3122  df-rex 3123  df-v 3416  df-in 3805  df-ss 3812  df-sn 4398  df-iun 4742

This theorem is referenced by:  iunxpconst  5408  fvn0ssdmfun  6599  abnexg  7225  xpexgALT  7421  uniqs  8072  rankcf  9914  dprd2da  18795  t1ficld  21502  discmp  21572  xkoinjcn  21861  metnrmlem2  23033  ovoliunlem1  23668  i1fima  23844  i1fd  23847  itg1addlem5  23866  sibfof  30936  bnj1415  31641  cvmlift2lem12  31831  dftrpred4g  32261  poimirlem30  33976  itg2addnclem2  33998  ftc1anclem6  34026  uniqsALTV  34642  salexct3  41344  salgensscntex  41346  ctvonmbl  41690  vonct  41694