Theorem uniiun 4988

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

Syntax hints:   = wceq 1539  {cab 2715  ∃wrex 3065  ∪ cuni 4839  ∪ ciun 4924

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-rex 3070  df-uni 4840  df-iun 4926

This theorem is referenced by:  iununi  5028  iunpwss  5036  truni  5205  reluni  5728  rnuni  6052  imauni  7119  iunpw  7621  oa0r  8368  om1r  8374  oeworde  8424  unifi  9108  infssuni  9110  cfslb2n  10024  ituniiun  10178  unidom  10299  unictb  10331  gruuni  10556  gruun  10562  hashuni  15538  tgidm  22130  unicld  22197  clsval2  22201  mretopd  22243  tgrest  22310  cmpsublem  22550  cmpsub  22551  tgcmp  22552  hauscmplem  22557  cmpfi  22559  unconn  22580  conncompconn  22583  comppfsc  22683  kgentopon  22689  txbasval  22757  txtube  22791  txcmplem1  22792  txcmplem2  22793  xkococnlem  22810  alexsublem  23195  alexsubALT  23202  opnmblALT  24767  limcun  25059  uniin1  30891  uniin2  30892  disjuniel  30936  hashunif  31126  dmvlsiga  32097  measinblem  32188  volmeas  32199  carsggect  32285  omsmeas  32290  cvmscld  33235  istotbnd3  35929  sstotbnd  35933  heiborlem3  35971  heibor  35979  fiunicl  42615  founiiun  42715  founiiun0  42728  psmeasurelem  44008