Theorem uniiun 4776

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

Syntax hints:   = wceq 1637  {cab 2803  ∃wrex 3108  ∪ cuni 4641  ∪ ciun 4723

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-ext 2795

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-rex 3113  df-uni 4642  df-iun 4725

This theorem is referenced by:  iununi  4813  iunpwss  4821  truni  4971  reluni  5454  rnuni  5766  imauni  6735  iunpw  7215  oa0r  7862  om1r  7867  oeworde  7917  unifi  8501  infssuni  8503  cfslb2n  9382  ituniiun  9536  unidom  9657  unictb  9689  gruuni  9914  gruun  9920  hashuni  14787  tgidm  21006  unicld  21072  clsval2  21076  mretopd  21118  tgrest  21185  cmpsublem  21424  cmpsub  21425  tgcmp  21426  hauscmplem  21431  cmpfi  21433  unconn  21454  conncompconn  21457  comppfsc  21557  kgentopon  21563  txbasval  21631  txtube  21665  txcmplem1  21666  txcmplem2  21667  xkococnlem  21684  alexsublem  22069  alexsubALT  22076  opnmblALT  23594  limcun  23883  uniin1  29702  uniin2  29703  disjuniel  29745  hashunif  29899  dmvlsiga  30527  measinblem  30618  volmeas  30629  carsggect  30715  omsmeas  30720  cvmscld  31587  istotbnd3  33887  sstotbnd  33891  heiborlem3  33929  heibor  33937  fiunicl  39734  founiiun  39854  founiiun0  39871  psmeasurelem  41171