Theorem uniiun 5016

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

This proof depends on syntax axioms:   = wceq 1569  {cab 2738  ∃wrex 3086  ∪ cuni 4866  ∪ ciun 4950

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-rex 3087  df-uni 4867  df-iun 4952

This theorem is used by:  uniin1  5032  uniin2  5033  iununi  5058  iunpwss  5066  truni  5227  reluni  5795  rnuni  6139  imauni  7251  iunpw  7786  oa0r  8550  om1r  8555  oeworde  8606  unifi  9337  infssuni  9339  cfslb2n  10350  ituniiun  10504  unidom  10631  unictb  10664  gruuni  10889  gruun  10895  hashuni  15999  tgidm  23304  unicld  23370  clsval2  23374  mretopd  23416  tgrest  23483  cmpsublem  23723  cmpsub  23724  tgcmp  23725  hauscmplem  23730  cmpfi  23732  unconn  23753  conncompconn  23756  comppfsc  23857  kgentopon  23863  txbasval  23931  txtube  23965  txcmplem1  23966  txcmplem2  23967  xkococnlem  23984  alexsublem  24369  alexsubALT  24376  opnmblALT  25930  limcun  26221  disjuniel  33239  hashunif  33445  dmvlsiga  34808  measinblem  34900  volmeas  34911  carsggect  34997  omsmeas  35002  tz9.1regs  35859  cvmscld  36125  istotbnd3  38799  sstotbnd  38803  heiborlem3  38841  heibor  38849  limiun  44378  fiunicl  46178  founiiun  46288  founiiun0  46299  psmeasurelem  47574