Theorem uniiun 4808

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

Syntax hints:   = wceq 1601  {cab 2763  ∃wrex 3091  ∪ cuni 4673  ∪ ciun 4755

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-tru 1605  df-ex 1824  df-sb 2012  df-clab 2764  df-cleq 2770  df-rex 3096  df-uni 4674  df-iun 4757

This theorem is referenced by:  iununi  4846  iunpwss  4854  truni  5003  reluni  5491  rnuni  5800  imauni  6778  iunpw  7258  oa0r  7904  om1r  7909  oeworde  7959  unifi  8545  infssuni  8547  cfslb2n  9427  ituniiun  9581  unidom  9702  unictb  9734  gruuni  9959  gruun  9965  hashuni  14966  tgidm  21196  unicld  21262  clsval2  21266  mretopd  21308  tgrest  21375  cmpsublem  21615  cmpsub  21616  tgcmp  21617  hauscmplem  21622  cmpfi  21624  unconn  21645  conncompconn  21648  comppfsc  21748  kgentopon  21754  txbasval  21822  txtube  21856  txcmplem1  21857  txcmplem2  21858  xkococnlem  21875  alexsublem  22260  alexsubALT  22267  opnmblALT  23811  limcun  24100  uniin1  29934  uniin2  29935  disjuniel  29977  hashunif  30130  dmvlsiga  30794  measinblem  30885  volmeas  30896  carsggect  30982  omsmeas  30987  cvmscld  31858  istotbnd3  34199  sstotbnd  34203  heiborlem3  34241  heibor  34249  fiunicl  40177  founiiun  40294  founiiun0  40310  psmeasurelem  41621