Theorem iunxsn 5043

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  Vcvv 3438  {csn 4577  ∪ ciun 4943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3050  df-rex 3059  df-v 3440  df-sn 4578  df-iun 4945

This theorem is referenced by:  iunsuc  6401  funopsn  7090  fparlem3  8053  fparlem4  8054  iunfi  9237  kmlem11  10062  ackbij1lem8  10127  dfid6  14945  fsum2dlem  15687  fsumiun  15738  fprod2dlem  15897  prmreclem4  16841  fiuncmp  23329  ovolfiniun  25439  finiunmbl  25482  volfiniun  25485  voliunlem1  25488  iuninc  32551  cvmliftlem10  35349  mrsubvrs  35577  dfrcl4  43783  iunrelexp0  43809  corclrcl  43814  cotrcltrcl  43832  trclfvdecomr  43835  dfrtrcl4  43845  corcltrcl  43846  cotrclrcl  43849  imaf1hom  49223