Theorem uniiun 5034

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

Syntax hints:   = wceq 1540  {cab 2713  ∃wrex 3060  ∪ cuni 4883  ∪ ciun 4967

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-rex 3061  df-uni 4884  df-iun 4969

This theorem is referenced by:  iununi  5075  iunpwss  5083  truni  5245  reluni  5797  rnuni  6137  imauni  7238  iunpw  7765  oa0r  8550  om1r  8555  oeworde  8605  unifi  9356  infssuni  9358  cfslb2n  10282  ituniiun  10436  unidom  10557  unictb  10589  gruuni  10814  gruun  10820  hashuni  15842  tgidm  22918  unicld  22984  clsval2  22988  mretopd  23030  tgrest  23097  cmpsublem  23337  cmpsub  23338  tgcmp  23339  hauscmplem  23344  cmpfi  23346  unconn  23367  conncompconn  23370  comppfsc  23470  kgentopon  23476  txbasval  23544  txtube  23578  txcmplem1  23579  txcmplem2  23580  xkococnlem  23597  alexsublem  23982  alexsubALT  23989  opnmblALT  25556  limcun  25848  uniin1  32532  uniin2  32533  disjuniel  32578  hashunif  32785  dmvlsiga  34160  measinblem  34251  volmeas  34262  carsggect  34350  omsmeas  34355  cvmscld  35295  istotbnd3  37795  sstotbnd  37799  heiborlem3  37837  heibor  37845  limiun  43306  fiunicl  45091  founiiun  45203  founiiun0  45214  psmeasurelem  46499