Theorem iunxsn 4398

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 4397	. 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 1398   e. wcel 1823   _Vcvv 3106   {csn 4016   U_ciun 4315

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2809  df-rex 2810  df-v 3108  df-sbc 3325  df-sn 4017  df-iun 4317

This theorem is referenced by:  iunsuc  4949  fparlem3  6875  fparlem4  6876  iunfi  7800  kmlem11  8531  ackbij1lem8  8598  fsum2dlem  13667  fsumiun  13717  fprod2dlem  13866  prmreclem4  14521  fiuncmp  20071  ovolfiniun  22078  finiunmbl  22120  volfiniun  22123  voliunlem1  22126  iuninc  27638  cvmliftlem10  29003  mrsubvrs  29146  dfid6  38196  dfrcl4  38197  dfrtrcl4  38215  iunrelexp0  38224  corclrcl  38230  corcltrcl  38231  cotrclrcl  38232  cotrcltrcl  38233