Theorem iunxsn 5038

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

Syntax hints:   → wi 4   = wceq 1550   ∈ wcel 2132  Vcvv 3444  {csn 4572  ∪ ciun 4939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1553  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-ral 3067  df-rex 3077  df-v 3446  df-sn 4573  df-iun 4941

This theorem is referenced by:  iunsuc  6418  funopsn  7115  funopsnOLD  7116  fparlem3  8077  fparlem4  8078  iunfi  9272  kmlem11  10103  ackbij1lem8  10168  dfid6  15027  fsum2dlem  15769  fsumiun  15821  fprod2dlem  15982  prmreclem4  16927  fiuncmp  23433  ovolfiniun  25532  finiunmbl  25575  volfiniun  25578  voliunlem1  25581  iuninc  32698  cvmliftlem10  35582  mrsubvrs  35810  dfrcl4  44190  iunrelexp0  44216  corclrcl  44221  cotrcltrcl  44239  trclfvdecomr  44242  dfrtrcl4  44252  corcltrcl  44253  cotrclrcl  44256  imaf1hom  49667