Theorem uniiun 5025

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

This proof depends on syntax axioms:   = wceq 1570  {cab 2743  ∃wrex 3091  ∪ cuni 4874  ∪ ciun 4958

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 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-rex 3092  df-uni 4875  df-iun 4960

This theorem is used by:  uniin1  5041  uniin2  5042  iununi  5067  iunpwss  5075  truni  5236  reluni  5807  rnuni  6148  imauni  7246  iunpw  7772  oa0r  8525  om1r  8530  oeworde  8581  unifi  9304  infssuni  9306  cfslb2n  10263  ituniiun  10417  unidom  10538  unictb  10571  gruuni  10796  gruun  10802  hashuni  15896  tgidm  23166  unicld  23232  clsval2  23236  mretopd  23278  tgrest  23345  cmpsublem  23585  cmpsub  23586  tgcmp  23587  hauscmplem  23592  cmpfi  23594  unconn  23615  conncompconn  23618  comppfsc  23718  kgentopon  23724  txbasval  23792  txtube  23826  txcmplem1  23827  txcmplem2  23828  xkococnlem  23845  alexsublem  24230  alexsubALT  24237  opnmblALT  25791  limcun  26083  disjuniel  32971  hashunif  33180  dmvlsiga  34542  measinblem  34634  volmeas  34645  carsggect  34732  omsmeas  34737  tz9.1regs  35563  cvmscld  35778  istotbnd3  38455  sstotbnd  38459  heiborlem3  38497  heibor  38505  limiun  44042  fiunicl  45820  founiiun  45930  founiiun0  45941  psmeasurelem  47217