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

Theorem uniiun 4957
 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 4815 . 2 𝐴 = {𝑦 ∣ ∃𝑥𝐴 𝑦𝑥}
2 df-iun 4896 . 2 𝑥𝐴 𝑥 = {𝑦 ∣ ∃𝑥𝐴 𝑦𝑥}
31, 2eqtr4i 2848 1 𝐴 = 𝑥𝐴 𝑥
 Colors of variables: wff setvar class Syntax hints:   = wceq 1538  {cab 2800  ∃wrex 3131  ∪ cuni 4813  ∪ ciun 4894 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2794 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2801  df-cleq 2815  df-rex 3136  df-uni 4814  df-iun 4896 This theorem is referenced by:  iununi  4996  iunpwss  5004  truni  5162  reluni  5668  rnuni  5985  imauni  6988  iunpw  7478  oa0r  8150  om1r  8156  oeworde  8206  unifi  8801  infssuni  8803  cfslb2n  9679  ituniiun  9833  unidom  9954  unictb  9986  gruuni  10211  gruun  10217  hashuni  15172  tgidm  21583  unicld  21649  clsval2  21653  mretopd  21695  tgrest  21762  cmpsublem  22002  cmpsub  22003  tgcmp  22004  hauscmplem  22009  cmpfi  22011  unconn  22032  conncompconn  22035  comppfsc  22135  kgentopon  22141  txbasval  22209  txtube  22243  txcmplem1  22244  txcmplem2  22245  xkococnlem  22262  alexsublem  22647  alexsubALT  22654  opnmblALT  24205  limcun  24496  uniin1  30310  uniin2  30311  disjuniel  30355  hashunif  30538  dmvlsiga  31462  measinblem  31553  volmeas  31564  carsggect  31650  omsmeas  31655  cvmscld  32594  istotbnd3  35167  sstotbnd  35171  heiborlem3  35209  heibor  35217  fiunicl  41635  founiiun  41740  founiiun0  41755  psmeasurelem  43048
 Copyright terms: Public domain W3C validator