Theorem uniiun 5023

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

This proof depends on syntax axioms:   = wceq 1570  {cab 2741  ∃wrex 3089  ∪ cuni 4872  ∪ ciun 4956

This proof depends on 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 proof 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 4873  df-iun 4958

This theorem is used by:  uniin1  5039  uniin2  5040  iununi  5065  iunpwss  5073  truni  5234  reluni  5805  rnuni  6146  imauni  7244  iunpw  7766  oa0r  8519  om1r  8524  oeworde  8575  unifi  9297  infssuni  9299  cfslb2n  10256  ituniiun  10410  unidom  10531  unictb  10564  gruuni  10789  gruun  10795  hashuni  15883  tgidm  23146  unicld  23212  clsval2  23216  mretopd  23258  tgrest  23325  cmpsublem  23565  cmpsub  23566  tgcmp  23567  hauscmplem  23572  cmpfi  23574  unconn  23595  conncompconn  23598  comppfsc  23698  kgentopon  23704  txbasval  23772  txtube  23806  txcmplem1  23807  txcmplem2  23808  xkococnlem  23825  alexsublem  24210  alexsubALT  24217  opnmblALT  25771  limcun  26063  disjuniel  32951  hashunif  33160  dmvlsiga  34528  measinblem  34619  volmeas  34630  carsggect  34717  omsmeas  34722  tz9.1regs  35555  cvmscld  35773  istotbnd3  38450  sstotbnd  38454  heiborlem3  38492  heibor  38500  limiun  44037  fiunicl  45815  founiiun  45925  founiiun0  45936  psmeasurelem  47212