Theorem iunxsn 5056

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

Syntax hints:   → wi 4   = wceq 1568   ∈ wcel 2141  Vcvv 3453  {csn 4588  ∪ ciun 4955

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1571  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-v 3455  df-sn 4589  df-iun 4957

This theorem is referenced by:  iunsuc  6448  funopsn  7144  funopsnOLD  7145  fparlem3  8108  fparlem4  8109  iunfi  9299  kmlem11  10143  ackbij1lem8  10208  dfid6  15064  fsum2dlem  15820  fsumiun  15872  fprod2dlem  16033  prmreclem4  16978  fiuncmp  23540  ovolfiniun  25639  finiunmbl  25682  volfiniun  25685  voliunlem1  25688  iuninc  32871  cvmliftlem10  35740  mrsubvrs  35968  dfrcl4  44350  iunrelexp0  44376  corclrcl  44381  cotrcltrcl  44399  trclfvdecomr  44402  dfrtrcl4  44412  corcltrcl  44413  cotrclrcl  44416  imaf1hom  49831