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

Theorem uniiun 4564
 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 4429 . 2 𝐴 = {𝑦 ∣ ∃𝑥𝐴 𝑦𝑥}
2 df-iun 4513 . 2 𝑥𝐴 𝑥 = {𝑦 ∣ ∃𝑥𝐴 𝑦𝑥}
31, 2eqtr4i 2645 1 𝐴 = 𝑥𝐴 𝑥
 Colors of variables: wff setvar class Syntax hints:   = wceq 1481  {cab 2606  ∃wrex 2910  ∪ cuni 4427  ∪ ciun 4511 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-rex 2915  df-uni 4428  df-iun 4513 This theorem is referenced by:  iununi  4601  iunpwss  4609  truni  4758  reluni  5231  rnuni  5532  imauni  6489  iunpw  6963  oa0r  7603  om1r  7608  oeworde  7658  unifi  8240  infssuni  8242  cfslb2n  9075  ituniiun  9229  unidom  9350  unictb  9382  gruuni  9607  gruun  9613  hashuni  14539  tgidm  20765  unicld  20831  clsval2  20835  mretopd  20877  tgrest  20944  cmpsublem  21183  cmpsub  21184  tgcmp  21185  hauscmplem  21190  cmpfi  21192  unconn  21213  conncompconn  21216  comppfsc  21316  kgentopon  21322  txbasval  21390  txtube  21424  txcmplem1  21425  txcmplem2  21426  xkococnlem  21443  alexsublem  21829  alexsubALT  21836  opnmblALT  23352  limcun  23640  uniin1  29339  uniin2  29340  disjuniel  29382  hashunif  29536  dmvlsiga  30166  measinblem  30257  volmeas  30268  carsggect  30354  omsmeas  30359  cvmscld  31229  istotbnd3  33541  sstotbnd  33545  heiborlem3  33583  heibor  33591  fiunicl  39056  founiiun  39176  founiiun0  39193  psmeasurelem  40450
 Copyright terms: Public domain W3C validator