Theorem uniiun 5009

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

Syntax hints:   = wceq 1541  {cab 2711  ∃wrex 3057  ∪ cuni 4858  ∪ ciun 4941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-rex 3058  df-uni 4859  df-iun 4943

This theorem is referenced by:  iununi  5049  iunpwss  5057  truni  5215  reluni  5762  rnuni  6100  imauni  7186  iunpw  7710  oa0r  8459  om1r  8464  oeworde  8514  unifi  9235  infssuni  9237  cfslb2n  10166  ituniiun  10320  unidom  10441  unictb  10473  gruuni  10698  gruun  10704  hashuni  15735  tgidm  22896  unicld  22962  clsval2  22966  mretopd  23008  tgrest  23075  cmpsublem  23315  cmpsub  23316  tgcmp  23317  hauscmplem  23322  cmpfi  23324  unconn  23345  conncompconn  23348  comppfsc  23448  kgentopon  23454  txbasval  23522  txtube  23556  txcmplem1  23557  txcmplem2  23558  xkococnlem  23575  alexsublem  23960  alexsubALT  23967  opnmblALT  25532  limcun  25824  uniin1  32533  uniin2  32534  disjuniel  32579  hashunif  32793  dmvlsiga  34163  measinblem  34254  volmeas  34265  carsggect  34352  omsmeas  34357  tz9.1regs  35151  cvmscld  35338  istotbnd3  37831  sstotbnd  37835  heiborlem3  37873  heibor  37881  limiun  43399  fiunicl  45188  founiiun  45300  founiiun0  45311  psmeasurelem  46592