Theorem uniiun 4509

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

Syntax hints:   = wceq 1475  {cab 2596  ∃wrex 2897  ∪ cuni 4372  ∪ ciun 4455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-rex 2902  df-uni 4373  df-iun 4457

This theorem is referenced by:  iununi  4546  iunpwss  4551  truni  4695  reluni  5164  rnuni  5463  imauni  6408  iunpw  6870  oa0r  7505  om1r  7510  oeworde  7560  unifi  8138  infssuni  8140  cfslb2n  8973  ituniiun  9127  unidom  9244  unictb  9276  gruuni  9501  gruun  9507  hashuni  14397  tgidm  20595  unicld  20660  clsval2  20664  mretopd  20706  tgrest  20773  cmpsublem  21012  cmpsub  21013  tgcmp  21014  hauscmplem  21019  cmpfi  21021  uncon  21042  concompcon  21045  comppfsc  21145  kgentopon  21151  txbasval  21219  txtube  21253  txcmplem1  21254  txcmplem2  21255  xkococnlem  21272  alexsublem  21658  alexsubALT  21665  opnmblALT  23177  limcun  23465  uniin1  28750  uniin2  28751  disjuniel  28792  hashunif  28949  dmvlsiga  29519  measinblem  29610  volmeas  29621  carsggect  29707  omsmeas  29712  cvmscld  30509  istotbnd3  32740  sstotbnd  32744  heiborlem3  32782  heibor  32790  fiunicl  38261  founiiun  38355  founiiun0  38372  psmeasurelem  39363