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
iunxsn.2
Assertion
Ref Expression
iunxsn
Distinct variable groups:   ,   ,
Allowed substitution hint:   ()

Proof of Theorem iunxsn
StepHypRef Expression
1 iunxsn.1 . 2
2 iunxsn.2 . . 3
32iunxsng 4169 . 2
41, 3ax-mp 8 1
 Colors of variables: wff set class Syntax hints:   wi 4   wceq 1652   wcel 1725  cvv 2956  csn 3814  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