Theorem uniiun 5022

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

Syntax hints:   = wceq 1540  {cab 2707  ∃wrex 3053  ∪ cuni 4871  ∪ ciun 4955

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 4872  df-iun 4957

This theorem is referenced by:  iununi  5063  iunpwss  5071  truni  5230  reluni  5781  rnuni  6121  imauni  7220  iunpw  7747  oa0r  8502  om1r  8507  oeworde  8557  unifi  9295  infssuni  9297  cfslb2n  10221  ituniiun  10375  unidom  10496  unictb  10528  gruuni  10753  gruun  10759  hashuni  15792  tgidm  22867  unicld  22933  clsval2  22937  mretopd  22979  tgrest  23046  cmpsublem  23286  cmpsub  23287  tgcmp  23288  hauscmplem  23293  cmpfi  23295  unconn  23316  conncompconn  23319  comppfsc  23419  kgentopon  23425  txbasval  23493  txtube  23527  txcmplem1  23528  txcmplem2  23529  xkococnlem  23546  alexsublem  23931  alexsubALT  23938  opnmblALT  25504  limcun  25796  uniin1  32480  uniin2  32481  disjuniel  32526  hashunif  32731  dmvlsiga  34119  measinblem  34210  volmeas  34221  carsggect  34309  omsmeas  34314  cvmscld  35260  istotbnd3  37765  sstotbnd  37769  heiborlem3  37807  heibor  37815  limiun  43271  fiunicl  45061  founiiun  45173  founiiun0  45184  psmeasurelem  46468