MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iunxsn Structured version   Unicode version

Theorem iunxsn 4170
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
StepHypRef Expression
1 iunxsn.1 . 2  |-  A  e. 
_V
2 iunxsn.2 . . 3  |-  ( x  =  A  ->  B  =  C )
32iunxsng 4169 . 2  |-  ( A  e.  _V  ->  U_ x  e.  { A } B  =  C )
41, 3ax-mp 8 1  |-  U_ x  e.  { A } B  =  C
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    e. wcel 1725   _Vcvv 2956   {csn 3814   U_ciun 4093
This theorem is referenced by:  iunsuc  4663  fparlem3  6448  fparlem4  6449  iunfi  7394  kmlem11  8040  ackbij1lem8  8107  fsum2dlem  12554  fsumiun  12600  prmreclem4  13287  fiuncmp  17467  ovolfiniun  19397  finiunmbl  19438  volfiniun  19441  voliunlem1  19444  iuninc  24011  cvmliftlem10  24981  fprod2dlem  25304
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ral 2710  df-rex 2711  df-v 2958  df-sbc 3162  df-sn 3820  df-iun 4095
  Copyright terms: Public domain W3C validator