Theorem uniiun 5062

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

Syntax hints:   = wceq 1542  {cab 2710  ∃wrex 3071  ∪ cuni 4909  ∪ ciun 4998

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-rex 3072  df-uni 4910  df-iun 5000

This theorem is referenced by:  iununi  5103  iunpwss  5111  truni  5282  reluni  5819  rnuni  6149  imauni  7245  iunpw  7758  oa0r  8538  om1r  8543  oeworde  8593  unifi  9341  infssuni  9343  cfslb2n  10263  ituniiun  10417  unidom  10538  unictb  10570  gruuni  10795  gruun  10801  hashuni  15772  tgidm  22483  unicld  22550  clsval2  22554  mretopd  22596  tgrest  22663  cmpsublem  22903  cmpsub  22904  tgcmp  22905  hauscmplem  22910  cmpfi  22912  unconn  22933  conncompconn  22936  comppfsc  23036  kgentopon  23042  txbasval  23110  txtube  23144  txcmplem1  23145  txcmplem2  23146  xkococnlem  23163  alexsublem  23548  alexsubALT  23555  opnmblALT  25120  limcun  25412  uniin1  31814  uniin2  31815  disjuniel  31859  hashunif  32049  dmvlsiga  33158  measinblem  33249  volmeas  33260  carsggect  33348  omsmeas  33353  cvmscld  34295  istotbnd3  36687  sstotbnd  36691  heiborlem3  36729  heibor  36737  limiun  42080  fiunicl  43802  founiiun  43923  founiiun0  43936  psmeasurelem  45234