Theorem uniiun 4985

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

Syntax hints:   = wceq 1536  {cab 2802  ∃wrex 3142  ∪ cuni 4841  ∪ ciun 4922

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 1969  ax-7 2014  ax-9 2123  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780  df-sb 2069  df-clab 2803  df-cleq 2817  df-rex 3147  df-uni 4842  df-iun 4924

This theorem is referenced by:  iununi  5024  iunpwss  5032  truni  5189  reluni  5694  rnuni  6010  imauni  7008  iunpw  7496  oa0r  8166  om1r  8172  oeworde  8222  unifi  8816  infssuni  8818  cfslb2n  9693  ituniiun  9847  unidom  9968  unictb  10000  gruuni  10225  gruun  10231  hashuni  15184  tgidm  21591  unicld  21657  clsval2  21661  mretopd  21703  tgrest  21770  cmpsublem  22010  cmpsub  22011  tgcmp  22012  hauscmplem  22017  cmpfi  22019  unconn  22040  conncompconn  22043  comppfsc  22143  kgentopon  22149  txbasval  22217  txtube  22251  txcmplem1  22252  txcmplem2  22253  xkococnlem  22270  alexsublem  22655  alexsubALT  22662  opnmblALT  24207  limcun  24496  uniin1  30306  uniin2  30307  disjuniel  30350  hashunif  30531  dmvlsiga  31392  measinblem  31483  volmeas  31494  carsggect  31580  omsmeas  31585  cvmscld  32524  istotbnd3  35053  sstotbnd  35057  heiborlem3  35095  heibor  35103  fiunicl  41335  founiiun  41441  founiiun0  41457  psmeasurelem  42759