Theorem uniiun 4723

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

Syntax hints:   = wceq 1630  {cab 2744  ∃wrex 3049  ∪ cuni 4586  ∪ ciun 4670

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-clab 2745  df-cleq 2751  df-clel 2754  df-rex 3054  df-uni 4587  df-iun 4672

This theorem is referenced by:  iununi  4760  iunpwss  4768  truni  4917  reluni  5395  rnuni  5700  imauni  6665  iunpw  7141  oa0r  7785  om1r  7790  oeworde  7840  unifi  8418  infssuni  8420  cfslb2n  9280  ituniiun  9434  unidom  9555  unictb  9587  gruuni  9812  gruun  9818  hashuni  14755  tgidm  20984  unicld  21050  clsval2  21054  mretopd  21096  tgrest  21163  cmpsublem  21402  cmpsub  21403  tgcmp  21404  hauscmplem  21409  cmpfi  21411  unconn  21432  conncompconn  21435  comppfsc  21535  kgentopon  21541  txbasval  21609  txtube  21643  txcmplem1  21644  txcmplem2  21645  xkococnlem  21662  alexsublem  22047  alexsubALT  22054  opnmblALT  23569  limcun  23856  uniin1  29672  uniin2  29673  disjuniel  29715  hashunif  29869  dmvlsiga  30499  measinblem  30590  volmeas  30601  carsggect  30687  omsmeas  30692  cvmscld  31560  istotbnd3  33881  sstotbnd  33885  heiborlem3  33923  heibor  33931  fiunicl  39733  founiiun  39857  founiiun0  39874  psmeasurelem  41188