Theorem uniiun 5001

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

Syntax hints:   = wceq 1540  {cab 2714  ∃wrex 3071  ∪ cuni 4850  ∪ ciun 4937

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 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-rex 3072  df-uni 4851  df-iun 4939

This theorem is referenced by:  iununi  5041  iunpwss  5049  truni  5220  reluni  5747  rnuni  6074  imauni  7158  iunpw  7661  oa0r  8416  om1r  8422  oeworde  8472  unifi  9178  infssuni  9180  cfslb2n  10097  ituniiun  10251  unidom  10372  unictb  10404  gruuni  10629  gruun  10635  hashuni  15610  tgidm  22202  unicld  22269  clsval2  22273  mretopd  22315  tgrest  22382  cmpsublem  22622  cmpsub  22623  tgcmp  22624  hauscmplem  22629  cmpfi  22631  unconn  22652  conncompconn  22655  comppfsc  22755  kgentopon  22761  txbasval  22829  txtube  22863  txcmplem1  22864  txcmplem2  22865  xkococnlem  22882  alexsublem  23267  alexsubALT  23274  opnmblALT  24839  limcun  25131  uniin1  30999  uniin2  31000  disjuniel  31044  hashunif  31234  dmvlsiga  32203  measinblem  32294  volmeas  32305  carsggect  32391  omsmeas  32396  cvmscld  33340  istotbnd3  35985  sstotbnd  35989  heiborlem3  36027  heibor  36035  fiunicl  42836  founiiun  42943  founiiun0  42956  psmeasurelem  44246