Theorem uniiun 5024

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

Syntax hints:   = wceq 1570  {cab 2741  ∃wrex 3089  ∪ cuni 4873  ∪ ciun 4957

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-rex 3090  df-uni 4874  df-iun 4959

This theorem is referenced by:  uniin1  5040  uniin2  5041  iununi  5066  iunpwss  5074  truni  5235  reluni  5807  rnuni  6148  imauni  7246  iunpw  7771  oa0r  8524  om1r  8529  oeworde  8580  unifi  9302  infssuni  9304  cfslb2n  10253  ituniiun  10407  unidom  10528  unictb  10561  gruuni  10786  gruun  10792  hashuni  15880  tgidm  23118  unicld  23184  clsval2  23188  mretopd  23230  tgrest  23297  cmpsublem  23537  cmpsub  23538  tgcmp  23539  hauscmplem  23544  cmpfi  23546  unconn  23567  conncompconn  23570  comppfsc  23670  kgentopon  23676  txbasval  23744  txtube  23778  txcmplem1  23779  txcmplem2  23780  xkococnlem  23797  alexsublem  24182  alexsubALT  24189  opnmblALT  25743  limcun  26035  disjuniel  32923  hashunif  33132  dmvlsiga  34500  measinblem  34591  volmeas  34602  carsggect  34689  omsmeas  34694  tz9.1regs  35528  cvmscld  35746  istotbnd3  38403  sstotbnd  38407  heiborlem3  38445  heibor  38453  limiun  43992  fiunicl  45770  founiiun  45880  founiiun0  45891  psmeasurelem  47167