Theorem iunxsn 5034

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3430  {csn 4568  ∪ ciun 4934

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-v 3432  df-sn 4569  df-iun 4936

This theorem is referenced by:  iunsuc  6411  funopsn  7102  fparlem3  8064  fparlem4  8065  iunfi  9253  kmlem11  10083  ackbij1lem8  10148  dfid6  14990  fsum2dlem  15732  fsumiun  15784  fprod2dlem  15945  prmreclem4  16890  fiuncmp  23369  ovolfiniun  25468  finiunmbl  25511  volfiniun  25514  voliunlem1  25517  iuninc  32630  cvmliftlem10  35476  mrsubvrs  35704  dfrcl4  44103  iunrelexp0  44129  corclrcl  44134  cotrcltrcl  44152  trclfvdecomr  44155  dfrtrcl4  44165  corcltrcl  44166  cotrclrcl  44169  imaf1hom  49577