Theorem uniiun 5025

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

Syntax hints:   = wceq 1540  {cab 2708  ∃wrex 3054  ∪ cuni 4874  ∪ ciun 4958

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-rex 3055  df-uni 4875  df-iun 4960

This theorem is referenced by:  iununi  5066  iunpwss  5074  truni  5233  reluni  5784  rnuni  6124  imauni  7223  iunpw  7750  oa0r  8505  om1r  8510  oeworde  8560  unifi  9302  infssuni  9304  cfslb2n  10228  ituniiun  10382  unidom  10503  unictb  10535  gruuni  10760  gruun  10766  hashuni  15799  tgidm  22874  unicld  22940  clsval2  22944  mretopd  22986  tgrest  23053  cmpsublem  23293  cmpsub  23294  tgcmp  23295  hauscmplem  23300  cmpfi  23302  unconn  23323  conncompconn  23326  comppfsc  23426  kgentopon  23432  txbasval  23500  txtube  23534  txcmplem1  23535  txcmplem2  23536  xkococnlem  23553  alexsublem  23938  alexsubALT  23945  opnmblALT  25511  limcun  25803  uniin1  32487  uniin2  32488  disjuniel  32533  hashunif  32738  dmvlsiga  34126  measinblem  34217  volmeas  34228  carsggect  34316  omsmeas  34321  cvmscld  35267  istotbnd3  37772  sstotbnd  37776  heiborlem3  37814  heibor  37822  limiun  43278  fiunicl  45068  founiiun  45180  founiiun0  45191  psmeasurelem  46475