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

Theorem iunxsn 4792
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 4791 . 2 (𝐴 ∈ V → 𝑥 ∈ {𝐴}𝐵 = 𝐶)
41, 3ax-mp 5 1 𝑥 ∈ {𝐴}𝐵 = 𝐶
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1653  wcel 2157  Vcvv 3384  {csn 4367   ciun 4709
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2776
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2785  df-cleq 2791  df-clel 2794  df-nfc 2929  df-ral 3093  df-rex 3094  df-v 3386  df-sbc 3633  df-sn 4368  df-iun 4711
This theorem is referenced by:  iunsuc  6022  funopsn  6640  fparlem3  7515  fparlem4  7516  iunfi  8495  kmlem11  9269  ackbij1lem8  9336  dfid6  14106  fsum2dlem  14837  fsumiun  14888  fprod2dlem  15044  prmreclem4  15953  fiuncmp  21533  ovolfiniun  23606  finiunmbl  23649  volfiniun  23652  voliunlem1  23655  iuninc  29889  cvmliftlem10  31786  mrsubvrs  31929  dfrcl4  38740  iunrelexp0  38766  corclrcl  38771  cotrcltrcl  38789  trclfvdecomr  38792  dfrtrcl4  38802  corcltrcl  38803  cotrclrcl  38806
  Copyright terms: Public domain W3C validator