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

Theorem uniiun 4499
Description: Class union in terms of indexed union. Definition in [Stoll] p. 43. (Contributed by NM, 28-Jun-1998.)
Assertion
Ref Expression
uniiun 𝐴 = 𝑥𝐴 𝑥
Distinct variable group:   𝑥,𝐴

Proof of Theorem uniiun
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 dfuni2 4364 . 2 𝐴 = {𝑦 ∣ ∃𝑥𝐴 𝑦𝑥}
2 df-iun 4447 . 2 𝑥𝐴 𝑥 = {𝑦 ∣ ∃𝑥𝐴 𝑦𝑥}
31, 2eqtr4i 2630 1 𝐴 = 𝑥𝐴 𝑥
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  {cab 2591  wrex 2892   cuni 4362   ciun 4445
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-rex 2897  df-uni 4363  df-iun 4447
This theorem is referenced by:  iununi  4536  iunpwss  4541  truni  4685  reluni  5149  rnuni  5445  imauni  6382  iunpw  6843  oa0r  7478  om1r  7483  oeworde  7533  unifi  8111  infssuni  8113  cfslb2n  8946  ituniiun  9100  unidom  9217  unictb  9249  gruuni  9474  gruun  9480  hashuni  14339  tgidm  20533  unicld  20598  clsval2  20602  mretopd  20644  tgrest  20711  cmpsublem  20950  cmpsub  20951  tgcmp  20952  hauscmplem  20957  cmpfi  20959  uncon  20980  concompcon  20983  comppfsc  21083  kgentopon  21089  txbasval  21157  txtube  21191  txcmplem1  21192  txcmplem2  21193  xkococnlem  21210  alexsublem  21596  alexsubALT  21603  opnmblALT  23090  limcun  23378  uniin1  28552  uniin2  28553  disjuniel  28594  hashunif  28751  dmvlsiga  29321  measinblem  29412  volmeas  29423  carsggect  29509  omsmeas  29514  cvmscld  30311  istotbnd3  32539  sstotbnd  32543  heiborlem3  32581  heibor  32589  fiunicl  38060  founiiun  38154  founiiun0  38171  psmeasurelem  39163
  Copyright terms: Public domain W3C validator