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

Theorem iunxsn 4410
 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:   ,   ,

Proof of Theorem iunxsn
StepHypRef Expression
1 iunxsn.1 . 2
2 iunxsn.2 . . 3
32iunxsng 4409 . 2
41, 3ax-mp 5 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  =wceq 1395  e.wcel 1818   cvv 3109  {csn 4029  U_ciun 4330 This theorem is referenced by:  iunsuc  4965  fparlem3  6902  fparlem4  6903  iunfi  7828  kmlem11  8561  ackbij1lem8  8628  fsum2dlem  13585  fsumiun  13635  fprod2dlem  13784  prmreclem4  14437  fiuncmp  19904  ovolfiniun  21912  finiunmbl  21954  volfiniun  21957  voliunlem1  21960  iuninc  27428  cvmliftlem10  28739  mrsubvrs  28882 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-v 3111  df-sbc 3328  df-sn 4030  df-iun 4332
 Copyright terms: Public domain W3C validator