Theorem uniiun 5065

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

Syntax hints:   = wceq 1533  {cab 2702  ∃wrex 3059  ∪ cuni 4912  ∪ ciun 5000

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-rex 3060  df-uni 4913  df-iun 5002

This theorem is referenced by:  iununi  5106  iunpwss  5114  truni  5285  reluni  5823  rnuni  6159  imauni  7260  iunpw  7778  oa0r  8567  om1r  8572  oeworde  8622  unifi  9381  infssuni  9383  cfslb2n  10307  ituniiun  10461  unidom  10582  unictb  10614  gruuni  10839  gruun  10845  hashuni  15825  tgidm  22966  unicld  23033  clsval2  23037  mretopd  23079  tgrest  23146  cmpsublem  23386  cmpsub  23387  tgcmp  23388  hauscmplem  23393  cmpfi  23395  unconn  23416  conncompconn  23419  comppfsc  23519  kgentopon  23525  txbasval  23593  txtube  23627  txcmplem1  23628  txcmplem2  23629  xkococnlem  23646  alexsublem  24031  alexsubALT  24038  opnmblALT  25615  limcun  25907  uniin1  32463  uniin2  32464  disjuniel  32508  hashunif  32699  dmvlsiga  33918  measinblem  34009  volmeas  34020  carsggect  34108  omsmeas  34113  cvmscld  35053  istotbnd3  37420  sstotbnd  37424  heiborlem3  37462  heibor  37470  limiun  42885  fiunicl  44605  founiiun  44723  founiiun0  44734  psmeasurelem  46028