Theorem iunxsn 4539

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

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977  Vcvv 3173  {csn 4125  ∪ ciun 4455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-v 3175  df-sbc 3403  df-sn 4126  df-iun 4457

This theorem is referenced by:  iunsuc  5724  funopsn  6319  fparlem3  7166  fparlem4  7167  iunfi  8137  kmlem11  8865  ackbij1lem8  8932  dfid6  13616  fsum2dlem  14343  fsumiun  14394  fprod2dlem  14549  prmreclem4  15461  fiuncmp  21017  ovolfiniun  23076  finiunmbl  23119  volfiniun  23122  voliunlem1  23125  iuninc  28761  cvmliftlem10  30530  mrsubvrs  30673  dfrcl4  36987  iunrelexp0  37013  corclrcl  37018  cotrcltrcl  37036  trclfvdecomr  37039  dfrtrcl4  37049  corcltrcl  37050  cotrclrcl  37053