Theorem iunxsn 5043

Description: A singleton index picks out an instance of an indexed union's argument. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Mario Carneiro, 25-Jun-2016.)

Hypotheses

Ref	Expression
iunxsn.1	⊢ 𝐴 ∈ V
iunxsn.2	⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)

Assertion

Ref	Expression
iunxsn	⊢ ∪ 𝑥 ∈ {𝐴}𝐵 = 𝐶

Distinct variable groups:   𝑥,𝐴   𝑥,𝐶

Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem iunxsn

Step	Hyp	Ref	Expression
1		iunxsn.1	. 2 ⊢ 𝐴 ∈ V
2		iunxsn.2	. . 3 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
3	2	iunxsng 5042	. 2 ⊢ (𝐴 ∈ V → ∪ 𝑥 ∈ {𝐴}𝐵 = 𝐶)
4	1, 3	ax-mp 5	1 ⊢ ∪ 𝑥 ∈ {𝐴}𝐵 = 𝐶

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3438  {csn 4579  ∪ ciun 4944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-v 3440  df-sn 4580  df-iun 4946

This theorem is referenced by:  iunsuc  6398  funopsn  7086  fparlem3  8054  fparlem4  8055  iunfi  9252  kmlem11  10074  ackbij1lem8  10139  dfid6  14954  fsum2dlem  15696  fsumiun  15747  fprod2dlem  15906  prmreclem4  16850  fiuncmp  23308  ovolfiniun  25419  finiunmbl  25462  volfiniun  25465  voliunlem1  25468  iuninc  32523  cvmliftlem10  35286  mrsubvrs  35514  dfrcl4  43669  iunrelexp0  43695  corclrcl  43700  cotrcltrcl  43718  trclfvdecomr  43721  dfrtrcl4  43731  corcltrcl  43732  cotrclrcl  43735  imaf1hom  49113