Theorem iunxsn 4976

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

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  Vcvv 3441  {csn 4525  ∪ ciun 4881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-v 3443  df-sbc 3721  df-sn 4526  df-iun 4883

This theorem is referenced by:  iunsuc  6241  funopsn  6887  fparlem3  7792  fparlem4  7793  iunfi  8796  kmlem11  9571  ackbij1lem8  9638  dfid6  14379  fsum2dlem  15117  fsumiun  15168  fprod2dlem  15326  prmreclem4  16245  fiuncmp  22009  ovolfiniun  24105  finiunmbl  24148  volfiniun  24151  voliunlem1  24154  iuninc  30324  cvmliftlem10  32654  mrsubvrs  32882  dfrcl4  40377  iunrelexp0  40403  corclrcl  40408  cotrcltrcl  40426  trclfvdecomr  40429  dfrtrcl4  40439  corcltrcl  40440  cotrclrcl  40443