Theorem uniiun 5007

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

Syntax hints:   = wceq 1541  {cab 2709  ∃wrex 3056  ∪ cuni 4859  ∪ ciun 4941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-rex 3057  df-uni 4860  df-iun 4943

This theorem is referenced by:  iununi  5047  iunpwss  5055  truni  5213  reluni  5758  rnuni  6095  imauni  7180  iunpw  7704  oa0r  8453  om1r  8458  oeworde  8508  unifi  9228  infssuni  9230  cfslb2n  10156  ituniiun  10310  unidom  10431  unictb  10463  gruuni  10688  gruun  10694  hashuni  15730  tgidm  22893  unicld  22959  clsval2  22963  mretopd  23005  tgrest  23072  cmpsublem  23312  cmpsub  23313  tgcmp  23314  hauscmplem  23319  cmpfi  23321  unconn  23342  conncompconn  23345  comppfsc  23445  kgentopon  23451  txbasval  23519  txtube  23553  txcmplem1  23554  txcmplem2  23555  xkococnlem  23572  alexsublem  23957  alexsubALT  23964  opnmblALT  25529  limcun  25821  uniin1  32526  uniin2  32527  disjuniel  32572  hashunif  32783  dmvlsiga  34137  measinblem  34228  volmeas  34239  carsggect  34326  omsmeas  34331  tz9.1regs  35118  cvmscld  35305  istotbnd3  37810  sstotbnd  37814  heiborlem3  37852  heibor  37860  limiun  43314  fiunicl  45103  founiiun  45215  founiiun0  45226  psmeasurelem  46507