Theorem iunxsn 5024

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2109  Vcvv 3430  {csn 4566  ∪ ciun 4929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-v 3432  df-sn 4567  df-iun 4931

This theorem is referenced by:  iunsuc  6345  funopsn  7014  fparlem3  7938  fparlem4  7939  iunfi  9068  kmlem11  9900  ackbij1lem8  9967  dfid6  14720  fsum2dlem  15463  fsumiun  15514  fprod2dlem  15671  prmreclem4  16601  fiuncmp  22536  ovolfiniun  24646  finiunmbl  24689  volfiniun  24692  voliunlem1  24695  iuninc  30879  cvmliftlem10  33235  mrsubvrs  33463  dfrcl4  41237  iunrelexp0  41263  corclrcl  41268  cotrcltrcl  41286  trclfvdecomr  41289  dfrtrcl4  41299  corcltrcl  41300  cotrclrcl  41303