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

Theorem iunid 5054
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 4990 . 2 𝑥𝐴 {𝑥} = {𝑦 ∣ ∃𝑥𝐴 𝑦 ∈ {𝑥}}
2 clel5 3648 . . . 4 (𝑦𝐴 ↔ ∃𝑥𝐴 𝑦 = 𝑥)
3 velsn 4637 . . . . 5 (𝑦 ∈ {𝑥} ↔ 𝑦 = 𝑥)
43rexbii 3086 . . . 4 (∃𝑥𝐴 𝑦 ∈ {𝑥} ↔ ∃𝑥𝐴 𝑦 = 𝑥)
52, 4bitr4i 278 . . 3 (𝑦𝐴 ↔ ∃𝑥𝐴 𝑦 ∈ {𝑥})
65eqabi 2861 . 2 𝐴 = {𝑦 ∣ ∃𝑥𝐴 𝑦 ∈ {𝑥}}
71, 6eqtr4i 2755 1 𝑥𝐴 {𝑥} = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1533  wcel 2098  {cab 2701  wrex 3062  {csn 4621   ciun 4988
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695
This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-rex 3063  df-v 3468  df-sn 4622  df-iun 4990
This theorem is referenced by:  iunxpconst  5739  fvn0ssdmfun  7067  abnexg  7737  xpexgALT  7962  uniqs  8768  rankcf  10769  dprd2da  19956  t1ficld  23155  discmp  23226  xkoinjcn  23515  metnrmlem2  24700  ovoliunlem1  25355  i1fima  25531  i1fd  25534  itg1addlem5  25554  fnpreimac  32368  gsumpart  32678  elrspunidl  33018  sibfof  33831  bnj1415  34540  cvmlift2lem12  34796  poimirlem30  37012  itg2addnclem2  37034  ftc1anclem6  37060  uniqsALTV  37692  salexct3  45568  salgensscntex  45570  ctvonmbl  45915  vonct  45919
  Copyright terms: Public domain W3C validator