Theorem uniiun 5062

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

Syntax hints:   = wceq 1539  {cab 2707  ∃wrex 3068  ∪ cuni 4909  ∪ ciun 4998

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 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-rex 3069  df-uni 4910  df-iun 5000

This theorem is referenced by:  iununi  5103  iunpwss  5111  truni  5282  reluni  5819  rnuni  6149  imauni  7249  iunpw  7762  oa0r  8542  om1r  8547  oeworde  8597  unifi  9345  infssuni  9347  cfslb2n  10267  ituniiun  10421  unidom  10542  unictb  10574  gruuni  10799  gruun  10805  hashuni  15778  tgidm  22705  unicld  22772  clsval2  22776  mretopd  22818  tgrest  22885  cmpsublem  23125  cmpsub  23126  tgcmp  23127  hauscmplem  23132  cmpfi  23134  unconn  23155  conncompconn  23158  comppfsc  23258  kgentopon  23264  txbasval  23332  txtube  23366  txcmplem1  23367  txcmplem2  23368  xkococnlem  23385  alexsublem  23770  alexsubALT  23777  opnmblALT  25354  limcun  25646  uniin1  32048  uniin2  32049  disjuniel  32093  hashunif  32283  dmvlsiga  33423  measinblem  33514  volmeas  33525  carsggect  33613  omsmeas  33618  cvmscld  34560  istotbnd3  36944  sstotbnd  36948  heiborlem3  36986  heibor  36994  limiun  42336  fiunicl  44057  founiiun  44178  founiiun0  44189  psmeasurelem  45486