Theorem uniiun 5017

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

This proof depends on syntax axioms:   = wceq 1570  {cab 2739  ∃wrex 3087  ∪ cuni 4867  ∪ ciun 4951

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-rex 3088  df-uni 4868  df-iun 4953

This theorem is used by:  uniin1  5033  uniin2  5034  iununi  5059  iunpwss  5067  truni  5228  reluni  5796  rnuni  6140  imauni  7248  iunpw  7783  oa0r  8539  om1r  8544  oeworde  8595  unifi  9326  infssuni  9328  cfslb2n  10339  ituniiun  10493  unidom  10620  unictb  10653  gruuni  10878  gruun  10884  hashuni  15986  tgidm  23291  unicld  23357  clsval2  23361  mretopd  23403  tgrest  23470  cmpsublem  23710  cmpsub  23711  tgcmp  23712  hauscmplem  23717  cmpfi  23719  unconn  23740  conncompconn  23743  comppfsc  23844  kgentopon  23850  txbasval  23918  txtube  23952  txcmplem1  23953  txcmplem2  23954  xkococnlem  23971  alexsublem  24356  alexsubALT  24363  opnmblALT  25917  limcun  26208  disjuniel  33184  hashunif  33391  dmvlsiga  34754  measinblem  34846  volmeas  34857  carsggect  34943  omsmeas  34948  tz9.1regs  35785  cvmscld  36017  istotbnd3  38685  sstotbnd  38689  heiborlem3  38727  heibor  38735  limiun  44268  fiunicl  46053  founiiun  46163  founiiun0  46174  psmeasurelem  47449