Theorem iunxsn 5055

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  Vcvv 3453  {csn 4587  ∪ ciun 4954

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-v 3455  df-sn 4588  df-iun 4956

This theorem is used by:  iunsuc  6449  funopsn  7147  funopsnOLD  7148  fparlem3  8114  fparlem4  8115  iunfi  9313  kmlem11  10166  ackbij1lem8  10231  dfid6  15103  fsum2dlem  15858  fsumiun  15910  fprod2dlem  16071  prmreclem4  17015  fiuncmp  23630  ovolfiniun  25730  finiunmbl  25773  volfiniun  25776  voliunlem1  25779  iuninc  33020  cvmliftlem10  35860  mrsubvrs  36088  dfrcl4  44503  iunrelexp0  44529  corclrcl  44534  cotrcltrcl  44552  trclfvdecomr  44555  dfrtrcl4  44565  corcltrcl  44566  cotrclrcl  44569  imaf1hom  50021