Theorem iunxsn 4375

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 4374	. 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 1455   e. wcel 1898   _Vcvv 3057   {csn 3980   U_ciun 4292

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ral 2754  df-rex 2755  df-v 3059  df-sbc 3280  df-sn 3981  df-iun 4294

This theorem is referenced by:  iunsuc  5528  fparlem3  6930  fparlem4  6931  iunfi  7893  kmlem11  8621  ackbij1lem8  8688  dfid6  13146  fsum2dlem  13886  fsumiun  13936  fprod2dlem  14089  prmreclem4  14918  fiuncmp  20474  ovolfiniun  22509  finiunmbl  22553  volfiniun  22556  voliunlem1  22559  iuninc  28230  cvmliftlem10  30067  mrsubvrs  30210  dfrcl4  36314  iunrelexp0  36340  corclrcl  36345  cotrcltrcl  36363  trclfvdecomr  36366  dfrtrcl4  36376  corcltrcl  36377  cotrclrcl  36380  funopsn  39156