Theorem uniiun 5013

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.

Step	Hyp	Ref	Expression
1		dfuni2 4864	. 2 ⊢ ∪ 𝐴 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝑥}
2		df-iun 4948	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝑥 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝑥}
3	1, 2	eqtr4i 2787	1 ⊢ ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝑥

Syntax hints:   = wceq 1559  {cab 2739  ∃wrex 3085  ∪ cuni 4862  ∪ ciun 4946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-rex 3086  df-uni 4863  df-iun 4948

This theorem is referenced by:  iununi  5053  iunpwss  5061  truni  5220  reluni  5787  rnuni  6129  imauni  7225  iunpw  7749  oa0r  8501  om1r  8506  oeworde  8557  unifi  9281  infssuni  9283  cfslb2n  10219  ituniiun  10373  unidom  10494  unictb  10527  gruuni  10752  gruun  10758  hashuni  15845  tgidm  23028  unicld  23094  clsval2  23098  mretopd  23140  tgrest  23207  cmpsublem  23447  cmpsub  23448  tgcmp  23449  hauscmplem  23454  cmpfi  23456  unconn  23477  conncompconn  23480  comppfsc  23580  kgentopon  23586  txbasval  23654  txtube  23688  txcmplem1  23689  txcmplem2  23690  xkococnlem  23707  alexsublem  24092  alexsubALT  24099  opnmblALT  25653  limcun  25945  uniin1  32711  uniin2  32712  disjuniel  32757  hashunif  32969  dmvlsiga  34387  measinblem  34478  volmeas  34489  carsggect  34576  omsmeas  34581  tz9.1regs  35391  cvmscld  35584  istotbnd3  38231  sstotbnd  38235  heiborlem3  38273  heibor  38281  limiun  43820  fiunicl  45608  founiiun  45718  founiiun0  45729  psmeasurelem  47005