Theorem uniiun 5016

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

Syntax hints:   = wceq 1542  {cab 2715  ∃wrex 3062  ∪ cuni 4865  ∪ ciun 4948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-rex 3063  df-uni 4866  df-iun 4950

This theorem is referenced by:  iununi  5056  iunpwss  5064  truni  5222  reluni  5775  rnuni  6114  imauni  7202  iunpw  7726  oa0r  8475  om1r  8480  oeworde  8531  unifi  9256  infssuni  9258  cfslb2n  10190  ituniiun  10344  unidom  10465  unictb  10498  gruuni  10723  gruun  10729  hashuni  15761  tgidm  22936  unicld  23002  clsval2  23006  mretopd  23048  tgrest  23115  cmpsublem  23355  cmpsub  23356  tgcmp  23357  hauscmplem  23362  cmpfi  23364  unconn  23385  conncompconn  23388  comppfsc  23488  kgentopon  23494  txbasval  23562  txtube  23596  txcmplem1  23597  txcmplem2  23598  xkococnlem  23615  alexsublem  24000  alexsubALT  24007  opnmblALT  25572  limcun  25864  uniin1  32637  uniin2  32638  disjuniel  32683  hashunif  32896  dmvlsiga  34306  measinblem  34397  volmeas  34408  carsggect  34495  omsmeas  34500  tz9.1regs  35309  cvmscld  35486  istotbnd3  38016  sstotbnd  38020  heiborlem3  38058  heibor  38066  limiun  43633  fiunicl  45421  founiiun  45532  founiiun0  45543  psmeasurelem  46822