Theorem uniiun 5058

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

Syntax hints:   = wceq 1540  {cab 2714  ∃wrex 3070  ∪ cuni 4907  ∪ ciun 4991

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 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-rex 3071  df-uni 4908  df-iun 4993

This theorem is referenced by:  iununi  5099  iunpwss  5107  truni  5275  reluni  5828  rnuni  6168  imauni  7266  iunpw  7791  oa0r  8576  om1r  8581  oeworde  8631  unifi  9384  infssuni  9386  cfslb2n  10308  ituniiun  10462  unidom  10583  unictb  10615  gruuni  10840  gruun  10846  hashuni  15862  tgidm  22987  unicld  23054  clsval2  23058  mretopd  23100  tgrest  23167  cmpsublem  23407  cmpsub  23408  tgcmp  23409  hauscmplem  23414  cmpfi  23416  unconn  23437  conncompconn  23440  comppfsc  23540  kgentopon  23546  txbasval  23614  txtube  23648  txcmplem1  23649  txcmplem2  23650  xkococnlem  23667  alexsublem  24052  alexsubALT  24059  opnmblALT  25638  limcun  25930  uniin1  32564  uniin2  32565  disjuniel  32610  hashunif  32810  dmvlsiga  34130  measinblem  34221  volmeas  34232  carsggect  34320  omsmeas  34325  cvmscld  35278  istotbnd3  37778  sstotbnd  37782  heiborlem3  37820  heibor  37828  limiun  43295  fiunicl  45072  founiiun  45184  founiiun0  45195  psmeasurelem  46485