Theorem iunxsn 5022

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3427  {csn 4557  ∪ ciun 4923

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-ral 3050  df-rex 3060  df-v 3429  df-sn 4558  df-iun 4925

This theorem is referenced by:  iunsuc  6399  funopsn  7090  funopsnOLD  7091  fparlem3  8053  fparlem4  8054  iunfi  9242  kmlem11  10072  ackbij1lem8  10137  dfid6  14979  fsum2dlem  15721  fsumiun  15773  fprod2dlem  15934  prmreclem4  16879  fiuncmp  23357  ovolfiniun  25456  finiunmbl  25499  volfiniun  25502  voliunlem1  25505  iuninc  32618  cvmliftlem10  35464  mrsubvrs  35692  dfrcl4  44091  iunrelexp0  44117  corclrcl  44122  cotrcltrcl  44140  trclfvdecomr  44143  dfrtrcl4  44153  corcltrcl  44154  cotrclrcl  44157  imaf1hom  49571