Theorem iunxsn 4792

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

Syntax hints:   → wi 4   = wceq 1653   ∈ wcel 2157  Vcvv 3384  {csn 4367  ∪ ciun 4709

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2776

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2785  df-cleq 2791  df-clel 2794  df-nfc 2929  df-ral 3093  df-rex 3094  df-v 3386  df-sbc 3633  df-sn 4368  df-iun 4711

This theorem is referenced by:  iunsuc  6022  funopsn  6640  fparlem3  7515  fparlem4  7516  iunfi  8495  kmlem11  9269  ackbij1lem8  9336  dfid6  14106  fsum2dlem  14837  fsumiun  14888  fprod2dlem  15044  prmreclem4  15953  fiuncmp  21533  ovolfiniun  23606  finiunmbl  23649  volfiniun  23652  voliunlem1  23655  iuninc  29889  cvmliftlem10  31786  mrsubvrs  31929  dfrcl4  38740  iunrelexp0  38766  corclrcl  38771  cotrcltrcl  38789  trclfvdecomr  38792  dfrtrcl4  38802  corcltrcl  38803  cotrclrcl  38806