Theorem iunxsn 5055

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 5054	. 2 ⊢ (𝐴 ∈ V → ∪ 𝑥 ∈ {𝐴}𝐵 = 𝐶)
4	1, 3	ax-mp 5	1 ⊢ ∪ 𝑥 ∈ {𝐴}𝐵 = 𝐶

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3447  {csn 4589  ∪ ciun 4955

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 3449  df-sn 4590  df-iun 4957

This theorem is referenced by:  iunsuc  6419  funopsn  7120  fparlem3  8093  fparlem4  8094  iunfi  9294  kmlem11  10114  ackbij1lem8  10179  dfid6  14994  fsum2dlem  15736  fsumiun  15787  fprod2dlem  15946  prmreclem4  16890  fiuncmp  23291  ovolfiniun  25402  finiunmbl  25445  volfiniun  25448  voliunlem1  25451  iuninc  32489  cvmliftlem10  35281  mrsubvrs  35509  dfrcl4  43665  iunrelexp0  43691  corclrcl  43696  cotrcltrcl  43714  trclfvdecomr  43717  dfrtrcl4  43727  corcltrcl  43728  cotrclrcl  43731  imaf1hom  49097