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

Theorem iunid 5065
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 4998 . 2 𝑥𝐴 {𝑥} = {𝑦 ∣ ∃𝑥𝐴 𝑦 ∈ {𝑥}}
2 clel5 3665 . . . 4 (𝑦𝐴 ↔ ∃𝑥𝐴 𝑦 = 𝑥)
3 velsn 4647 . . . . 5 (𝑦 ∈ {𝑥} ↔ 𝑦 = 𝑥)
43rexbii 3092 . . . 4 (∃𝑥𝐴 𝑦 ∈ {𝑥} ↔ ∃𝑥𝐴 𝑦 = 𝑥)
52, 4bitr4i 278 . . 3 (𝑦𝐴 ↔ ∃𝑥𝐴 𝑦 ∈ {𝑥})
65eqabi 2875 . 2 𝐴 = {𝑦 ∣ ∃𝑥𝐴 𝑦 ∈ {𝑥}}
71, 6eqtr4i 2766 1 𝑥𝐴 {𝑥} = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1537  wcel 2106  {cab 2712  wrex 3068  {csn 4631   ciun 4996
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rex 3069  df-v 3480  df-sn 4632  df-iun 4998
This theorem is referenced by:  iunxpconst  5761  fvn0ssdmfun  7094  abnexg  7775  xpexgALT  8005  uniqs  8816  rankcf  10815  dprd2da  20077  t1ficld  23351  discmp  23422  xkoinjcn  23711  metnrmlem2  24896  ovoliunlem1  25551  i1fima  25727  i1fd  25730  itg1addlem5  25750  dmdju  32664  fnpreimac  32688  gsumpart  33043  elrspunidl  33436  sibfof  34322  bnj1415  35031  cvmlift2lem12  35299  poimirlem30  37637  itg2addnclem2  37659  ftc1anclem6  37685  uniqsALTV  38311  salexct3  46298  salgensscntex  46300  ctvonmbl  46645  vonct  46649
  Copyright terms: Public domain W3C validator