Theorem uniiun 5010

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 4863	. 2 ⊢ ∪ 𝐴 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝑥}
2		df-iun 4946	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝑥 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝑥}
3	1, 2	eqtr4i 2755	1 ⊢ ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝑥

Syntax hints:   = wceq 1540  {cab 2707  ∃wrex 3053  ∪ cuni 4861  ∪ ciun 4944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-rex 3054  df-uni 4862  df-iun 4946

This theorem is referenced by:  iununi  5051  iunpwss  5059  truni  5217  reluni  5765  rnuni  6101  imauni  7186  iunpw  7711  oa0r  8463  om1r  8468  oeworde  8518  unifi  9253  infssuni  9255  cfslb2n  10181  ituniiun  10335  unidom  10456  unictb  10488  gruuni  10713  gruun  10719  hashuni  15751  tgidm  22883  unicld  22949  clsval2  22953  mretopd  22995  tgrest  23062  cmpsublem  23302  cmpsub  23303  tgcmp  23304  hauscmplem  23309  cmpfi  23311  unconn  23332  conncompconn  23335  comppfsc  23435  kgentopon  23441  txbasval  23509  txtube  23543  txcmplem1  23544  txcmplem2  23545  xkococnlem  23562  alexsublem  23947  alexsubALT  23954  opnmblALT  25520  limcun  25812  uniin1  32513  uniin2  32514  disjuniel  32559  hashunif  32764  dmvlsiga  34095  measinblem  34186  volmeas  34197  carsggect  34285  omsmeas  34290  tz9.1regs  35066  cvmscld  35245  istotbnd3  37750  sstotbnd  37754  heiborlem3  37792  heibor  37800  limiun  43255  fiunicl  45045  founiiun  45157  founiiun0  45168  psmeasurelem  46452