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

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
StepHypRef Expression
1 iunxsn.1 . 2  |-  A  e. 
_V
2 iunxsn.2 . . 3  |-  ( x  =  A  ->  B  =  C )
32iunxsng 4356 . 2  |-  ( A  e.  _V  ->  U_ x  e.  { A } B  =  C )
41, 3ax-mp 5 1  |-  U_ x  e.  { A } B  =  C
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator