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

Theorem iunxsn 4635
 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 4634 . 2 (𝐴 ∈ V → 𝑥 ∈ {𝐴}𝐵 = 𝐶)
41, 3ax-mp 5 1 𝑥 ∈ {𝐴}𝐵 = 𝐶
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1523   ∈ wcel 2030  Vcvv 3231  {csn 4210  ∪ ciun 4552 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-v 3233  df-sbc 3469  df-sn 4211  df-iun 4554 This theorem is referenced by:  iunsuc  5845  funopsn  6453  fparlem3  7324  fparlem4  7325  iunfi  8295  kmlem11  9020  ackbij1lem8  9087  dfid6  13812  fsum2dlem  14545  fsumiun  14597  fprod2dlem  14754  prmreclem4  15670  fiuncmp  21255  ovolfiniun  23315  finiunmbl  23358  volfiniun  23361  voliunlem1  23364  iuninc  29505  cvmliftlem10  31402  mrsubvrs  31545  dfrcl4  38285  iunrelexp0  38311  corclrcl  38316  cotrcltrcl  38334  trclfvdecomr  38337  dfrtrcl4  38347  corcltrcl  38348  cotrclrcl  38351
 Copyright terms: Public domain W3C validator