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

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
StepHypRef Expression
1 iunxsn.1 . 2  |-  A  e. 
_V
2 iunxsn.2 . . 3  |-  ( x  =  A  ->  B  =  C )
32iunxsng 4397 . 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 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
  Copyright terms: Public domain W3C validator