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

Theorem iunid 5064
Description: An indexed union of singletons recovers the index set. (Contributed by NM, 6-Sep-2005.) (Proof shortened by SN, 15-Jan-2025.)
Assertion
Ref Expression
iunid 𝑥𝐴 {𝑥} = 𝐴
Distinct variable group:   𝑥,𝐴

Proof of Theorem iunid
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 df-iun 5000 . 2 𝑥𝐴 {𝑥} = {𝑦 ∣ ∃𝑥𝐴 𝑦 ∈ {𝑥}}
2 clel5 3656 . . . 4 (𝑦𝐴 ↔ ∃𝑥𝐴 𝑦 = 𝑥)
3 velsn 4645 . . . . 5 (𝑦 ∈ {𝑥} ↔ 𝑦 = 𝑥)
43rexbii 3095 . . . 4 (∃𝑥𝐴 𝑦 ∈ {𝑥} ↔ ∃𝑥𝐴 𝑦 = 𝑥)
52, 4bitr4i 278 . . 3 (𝑦𝐴 ↔ ∃𝑥𝐴 𝑦 ∈ {𝑥})
65eqabi 2870 . 2 𝐴 = {𝑦 ∣ ∃𝑥𝐴 𝑦 ∈ {𝑥}}
71, 6eqtr4i 2764 1 𝑥𝐴 {𝑥} = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  wcel 2107  {cab 2710  wrex 3071  {csn 4629   ciun 4998
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rex 3072  df-v 3477  df-sn 4630  df-iun 5000
This theorem is referenced by:  iunxpconst  5749  fvn0ssdmfun  7077  abnexg  7743  xpexgALT  7968  uniqs  8771  rankcf  10772  dprd2da  19912  t1ficld  22831  discmp  22902  xkoinjcn  23191  metnrmlem2  24376  ovoliunlem1  25019  i1fima  25195  i1fd  25198  itg1addlem5  25218  fnpreimac  31896  gsumpart  32207  elrspunidl  32546  sibfof  33339  bnj1415  34049  cvmlift2lem12  34305  poimirlem30  36518  itg2addnclem2  36540  ftc1anclem6  36566  uniqsALTV  37198  salexct3  45058  salgensscntex  45060  ctvonmbl  45405  vonct  45409
  Copyright terms: Public domain W3C validator