Theorem iunid 5021

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 4955	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥}}
2		clel5 3621	. . . 4 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑦 = 𝑥)
3		velsn 4599	. . . . 5 ⊢ (𝑦 ∈ {𝑥} ↔ 𝑦 = 𝑥)
4	3	rexbii 3112	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥} ↔ ∃𝑥 ∈ 𝐴 𝑦 = 𝑥)
5	2, 4	bitr4i 281	. . 3 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥})
6	5	eqabi 2898	. 2 ⊢ 𝐴 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥}}
7	1, 6	eqtr4i 2789	1 ⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = 𝐴

This proof depends on syntax axioms:   = wceq 1569   ∈ wcel 2146  {cab 2741  ∃wrex 3089  {csn 4587  ∪ ciun 4953

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-rex 3090  df-v 3455  df-sn 4588  df-iun 4955

This theorem is used by:  iunxpconst  5727  fvn0ssdmfun  7082  abnexg  7777  xpexgALT  8000  uniqs  8805  rankcf  10872  dprd2da  20270  t1ficld  23657  discmp  23728  xkoinjcn  24018  metnrmlem2  25192  ovoliunlem1  25835  i1fima  26011  i1fd  26014  itg1addlem5  26033  rnplynfin  26642  dmdju  33295  fnpreimac  33318  gsumpart  33677  elrspunidl  34031  sibfof  35025  bnj1415  35721  1enumen  35784  cvmlift2lem12  36200  poimirlem30  38708  itg2addnclem2  38730  ftc1anclem6  38756  salexct3  47491  salgensscntex  47493  ctvonmbl  47838  vonct  47842