Theorem iunxsn 5095

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  Vcvv 3475  {csn 4629  ∪ ciun 4998

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-v 3477  df-sn 4630  df-iun 5000

This theorem is referenced by:  iunsuc  6450  funopsn  7146  fparlem3  8100  fparlem4  8101  iunfi  9340  kmlem11  10155  ackbij1lem8  10222  dfid6  14975  fsum2dlem  15716  fsumiun  15767  fprod2dlem  15924  prmreclem4  16852  fiuncmp  22908  ovolfiniun  25018  finiunmbl  25061  volfiniun  25064  voliunlem1  25067  iuninc  31823  cvmliftlem10  34316  mrsubvrs  34544  dfrcl4  42475  iunrelexp0  42501  corclrcl  42506  cotrcltrcl  42524  trclfvdecomr  42527  dfrtrcl4  42537  corcltrcl  42538  cotrclrcl  42541