Theorem iunxsn 5054

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  Vcvv 3454  {csn 4588  ∪ 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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-v 3456  df-sn 4589  df-iun 4956

This theorem is used by:  iunsuc  6468  funopsn  7175  funopsnOLD  7176  fparlem3  8152  fparlem4  8153  iunfi  9360  kmlem11  10266  ackbij1lem8  10331  dfid6  15210  fsum2dlem  15965  fsumiun  16017  fprod2dlem  16176  prmreclem4  17126  fiuncmp  23752  ovolfiniun  25852  finiunmbl  25895  volfiniun  25898  voliunlem1  25901  iuninc  33227  cvmliftlem10  36226  mrsubvrs  36454  dfrcl4  44868  iunrelexp0  44894  corclrcl  44899  cotrcltrcl  44917  trclfvdecomr  44920  dfrtrcl4  44930  corcltrcl  44931  cotrclrcl  44934  imaf1hom  50429