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

Theorem iunid 5060
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 4993 . 2 𝑥𝐴 {𝑥} = {𝑦 ∣ ∃𝑥𝐴 𝑦 ∈ {𝑥}}
2 clel5 3665 . . . 4 (𝑦𝐴 ↔ ∃𝑥𝐴 𝑦 = 𝑥)
3 velsn 4642 . . . . 5 (𝑦 ∈ {𝑥} ↔ 𝑦 = 𝑥)
43rexbii 3094 . . . 4 (∃𝑥𝐴 𝑦 ∈ {𝑥} ↔ ∃𝑥𝐴 𝑦 = 𝑥)
52, 4bitr4i 278 . . 3 (𝑦𝐴 ↔ ∃𝑥𝐴 𝑦 ∈ {𝑥})
65eqabi 2877 . 2 𝐴 = {𝑦 ∣ ∃𝑥𝐴 𝑦 ∈ {𝑥}}
71, 6eqtr4i 2768 1 𝑥𝐴 {𝑥} = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1540  wcel 2108  {cab 2714  wrex 3070  {csn 4626   ciun 4991
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rex 3071  df-v 3482  df-sn 4627  df-iun 4993
This theorem is referenced by:  iunxpconst  5758  fvn0ssdmfun  7094  abnexg  7776  xpexgALT  8006  uniqs  8817  rankcf  10817  dprd2da  20062  t1ficld  23335  discmp  23406  xkoinjcn  23695  metnrmlem2  24882  ovoliunlem1  25537  i1fima  25713  i1fd  25716  itg1addlem5  25735  dmdju  32657  fnpreimac  32681  gsumpart  33060  elrspunidl  33456  sibfof  34342  bnj1415  35052  cvmlift2lem12  35319  poimirlem30  37657  itg2addnclem2  37679  ftc1anclem6  37705  uniqsALTV  38330  salexct3  46357  salgensscntex  46359  ctvonmbl  46704  vonct  46708
  Copyright terms: Public domain W3C validator