Theorem iunxsn 4357

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	|- A e. _V
iunxsn.2	|- ( x = A -> B = C )

Assertion

Ref	Expression
iunxsn	|- U_ x e. { A } B = C

Distinct variable groups:   x, A   x, C

Allowed substitution hint:   B( x)

Proof of Theorem iunxsn

Step	Hyp	Ref	Expression
1		iunxsn.1	. 2 |- A e. _V
2		iunxsn.2	. . 3 |- ( x = A -> B = C )
3	2	iunxsng 4356	. 2 |- ( A e. _V -> U_ x e. { A } B = C )
4	1, 3	ax-mp 5	1 |- U_ x e. { A } B = C

Syntax hints:   -> wi 4   = wceq 1370   e. wcel 1758   _Vcvv 3076   {csn 3984   U_ciun 4278

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2803  df-rex 2804  df-v 3078  df-sbc 3293  df-sn 3985  df-iun 4280

This theorem is referenced by:  iunsuc  4908  fparlem3  6783  fparlem4  6784  iunfi  7709  kmlem11  8439  ackbij1lem8  8506  fsum2dlem  13354  fsumiun  13401  prmreclem4  14097  fiuncmp  19138  ovolfiniun  21115  finiunmbl  21157  volfiniun  21160  voliunlem1  21163  iuninc  26061  cvmliftlem10  27326  fprod2dlem  27634