Theorem uniiun 5038

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

Syntax hints:   = wceq 1539  {cab 2712  ∃wrex 3059  ∪ cuni 4887  ∪ ciun 4971

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-rex 3060  df-uni 4888  df-iun 4973

This theorem is referenced by:  iununi  5079  iunpwss  5087  truni  5255  reluni  5808  rnuni  6148  imauni  7248  iunpw  7773  oa0r  8558  om1r  8563  oeworde  8613  unifi  9366  infssuni  9368  cfslb2n  10290  ituniiun  10444  unidom  10565  unictb  10597  gruuni  10822  gruun  10828  hashuni  15845  tgidm  22935  unicld  23001  clsval2  23005  mretopd  23047  tgrest  23114  cmpsublem  23354  cmpsub  23355  tgcmp  23356  hauscmplem  23361  cmpfi  23363  unconn  23384  conncompconn  23387  comppfsc  23487  kgentopon  23493  txbasval  23561  txtube  23595  txcmplem1  23596  txcmplem2  23597  xkococnlem  23614  alexsublem  23999  alexsubALT  24006  opnmblALT  25575  limcun  25867  uniin1  32500  uniin2  32501  disjuniel  32546  hashunif  32754  dmvlsiga  34105  measinblem  34196  volmeas  34207  carsggect  34295  omsmeas  34300  cvmscld  35253  istotbnd3  37753  sstotbnd  37757  heiborlem3  37795  heibor  37803  limiun  43272  fiunicl  45044  founiiun  45156  founiiun0  45167  psmeasurelem  46457