Theorem iunid 5065

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 5000	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥}}
2		clel5 3653	. . . 4 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑦 = 𝑥)
3		velsn 4646	. . . . 5 ⊢ (𝑦 ∈ {𝑥} ↔ 𝑦 = 𝑥)
4	3	rexbii 3090	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥} ↔ ∃𝑥 ∈ 𝐴 𝑦 = 𝑥)
5	2, 4	bitr4i 277	. . 3 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥})
6	5	eqabi 2864	. 2 ⊢ 𝐴 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥}}
7	1, 6	eqtr4i 2758	1 ⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = 𝐴

Syntax hints:   = wceq 1533   ∈ wcel 2098  {cab 2704  ∃wrex 3066  {csn 4630  ∪ ciun 4998

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2705  df-cleq 2719  df-clel 2805  df-rex 3067  df-v 3473  df-sn 4631  df-iun 5000

This theorem is referenced by:  iunxpconst  5752  fvn0ssdmfun  7087  abnexg  7762  xpexgALT  7989  uniqs  8800  rankcf  10806  dprd2da  20004  t1ficld  23249  discmp  23320  xkoinjcn  23609  metnrmlem2  24794  ovoliunlem1  25449  i1fima  25625  i1fd  25628  itg1addlem5  25648  fnpreimac  32475  gsumpart  32787  elrspunidl  33162  sibfof  33965  bnj1415  34674  cvmlift2lem12  34929  poimirlem30  37128  itg2addnclem2  37150  ftc1anclem6  37176  uniqsALTV  37805  salexct3  45732  salgensscntex  45734  ctvonmbl  46079  vonct  46083

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »