Theorem iunxsn 5049

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

Syntax hints:   → wi 4   = wceq 1561   ∈ wcel 2143  Vcvv 3455  {csn 4583  ∪ ciun 4950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1564  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3078  df-rex 3088  df-v 3457  df-sn 4584  df-iun 4952

This theorem is referenced by:  iunsuc  6433  funopsn  7130  funopsnOLD  7131  fparlem3  8093  fparlem4  8094  iunfi  9284  kmlem11  10128  ackbij1lem8  10193  dfid6  15051  fsum2dlem  15807  fsumiun  15859  fprod2dlem  16020  prmreclem4  16965  fiuncmp  23471  ovolfiniun  25570  finiunmbl  25613  volfiniun  25616  voliunlem1  25619  iuninc  32766  cvmliftlem10  35649  mrsubvrs  35877  dfrcl4  44257  iunrelexp0  44283  corclrcl  44288  cotrcltrcl  44306  trclfvdecomr  44309  dfrtrcl4  44319  corcltrcl  44320  cotrclrcl  44323  imaf1hom  49720