Theorem iunxsn 5037

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2110  Vcvv 3434  {csn 4574  ∪ ciun 4939

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 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-v 3436  df-sn 4575  df-iun 4941

This theorem is referenced by:  iunsuc  6389  funopsn  7076  fparlem3  8039  fparlem4  8040  iunfi  9222  kmlem11  10044  ackbij1lem8  10109  dfid6  14927  fsum2dlem  15669  fsumiun  15720  fprod2dlem  15879  prmreclem4  16823  fiuncmp  23312  ovolfiniun  25422  finiunmbl  25465  volfiniun  25468  voliunlem1  25471  iuninc  32530  cvmliftlem10  35306  mrsubvrs  35534  dfrcl4  43688  iunrelexp0  43714  corclrcl  43719  cotrcltrcl  43737  trclfvdecomr  43740  dfrtrcl4  43750  corcltrcl  43751  cotrclrcl  43754  imaf1hom  49119