Theorem iunxsn 5016

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  Vcvv 3422  {csn 4558  ∪ ciun 4921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-v 3424  df-sn 4559  df-iun 4923

This theorem is referenced by:  iunsuc  6333  funopsn  7002  fparlem3  7925  fparlem4  7926  iunfi  9037  kmlem11  9847  ackbij1lem8  9914  dfid6  14667  fsum2dlem  15410  fsumiun  15461  fprod2dlem  15618  prmreclem4  16548  fiuncmp  22463  ovolfiniun  24570  finiunmbl  24613  volfiniun  24616  voliunlem1  24619  iuninc  30801  cvmliftlem10  33156  mrsubvrs  33384  dfrcl4  41173  iunrelexp0  41199  corclrcl  41204  cotrcltrcl  41222  trclfvdecomr  41225  dfrtrcl4  41235  corcltrcl  41236  cotrclrcl  41239