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

Theorem iunxsn 4245
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 4244 . 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 1369    e. wcel 1756   _Vcvv 2967   {csn 3872   U_ciun 4166
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2715  df-rex 2716  df-v 2969  df-sbc 3182  df-sn 3873  df-iun 4168
This theorem is referenced by:  iunsuc  4796  fparlem3  6669  fparlem4  6670  iunfi  7591  kmlem11  8321  ackbij1lem8  8388  fsum2dlem  13229  fsumiun  13276  prmreclem4  13972  fiuncmp  18982  ovolfiniun  20959  finiunmbl  21000  volfiniun  21003  voliunlem1  21006  iuninc  25862  cvmliftlem10  27135  fprod2dlem  27442
  Copyright terms: Public domain W3C validator