Theorem iunxsn 5114

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  Vcvv 3488  {csn 4648  ∪ ciun 5015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-v 3490  df-sn 4649  df-iun 5017

This theorem is referenced by:  iunsuc  6480  funopsn  7182  fparlem3  8155  fparlem4  8156  iunfi  9411  kmlem11  10230  ackbij1lem8  10295  dfid6  15077  fsum2dlem  15818  fsumiun  15869  fprod2dlem  16028  prmreclem4  16966  fiuncmp  23433  ovolfiniun  25555  finiunmbl  25598  volfiniun  25601  voliunlem1  25604  iuninc  32583  cvmliftlem10  35262  mrsubvrs  35490  dfrcl4  43638  iunrelexp0  43664  corclrcl  43669  cotrcltrcl  43687  trclfvdecomr  43690  dfrtrcl4  43700  corcltrcl  43701  cotrclrcl  43704