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

Theorem iunxsn 4994
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 𝐴 ∈ V
iunxsn.2 (𝑥 = 𝐴𝐵 = 𝐶)
Assertion
Ref Expression
iunxsn 𝑥 ∈ {𝐴}𝐵 = 𝐶
Distinct variable groups:   𝑥,𝐴   𝑥,𝐶
Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem iunxsn
StepHypRef Expression
1 iunxsn.1 . 2 𝐴 ∈ V
2 iunxsn.2 . . 3 (𝑥 = 𝐴𝐵 = 𝐶)
32iunxsng 4993 . 2 (𝐴 ∈ V → 𝑥 ∈ {𝐴}𝐵 = 𝐶)
41, 3ax-mp 5 1 𝑥 ∈ {𝐴}𝐵 = 𝐶
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wcel 2115  Vcvv 3479  {csn 4548   ciun 4900
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ral 3137  df-rex 3138  df-v 3481  df-sbc 3758  df-sn 4549  df-iun 4902
This theorem is referenced by:  iunsuc  6254  funopsn  6891  fparlem3  7792  fparlem4  7793  iunfi  8796  kmlem11  9571  ackbij1lem8  9634  dfid6  14376  fsum2dlem  15114  fsumiun  15165  fprod2dlem  15323  prmreclem4  16242  fiuncmp  21998  ovolfiniun  24094  finiunmbl  24137  volfiniun  24140  voliunlem1  24143  iuninc  30309  cvmliftlem10  32559  mrsubvrs  32787  dfrcl4  40209  iunrelexp0  40235  corclrcl  40240  cotrcltrcl  40258  trclfvdecomr  40261  dfrtrcl4  40271  corcltrcl  40272  cotrclrcl  40275
  Copyright terms: Public domain W3C validator