Theorem uniiun 5002

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

Syntax hints:   = wceq 1542  {cab 2715  ∃wrex 3062  ∪ cuni 4851  ∪ ciun 4934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-rex 3063  df-uni 4852  df-iun 4936

This theorem is referenced by:  iununi  5042  iunpwss  5050  truni  5208  reluni  5767  rnuni  6106  imauni  7194  iunpw  7718  oa0r  8466  om1r  8471  oeworde  8522  unifi  9247  infssuni  9249  cfslb2n  10181  ituniiun  10335  unidom  10456  unictb  10489  gruuni  10714  gruun  10720  hashuni  15780  tgidm  22955  unicld  23021  clsval2  23025  mretopd  23067  tgrest  23134  cmpsublem  23374  cmpsub  23375  tgcmp  23376  hauscmplem  23381  cmpfi  23383  unconn  23404  conncompconn  23407  comppfsc  23507  kgentopon  23513  txbasval  23581  txtube  23615  txcmplem1  23616  txcmplem2  23617  xkococnlem  23634  alexsublem  24019  alexsubALT  24026  opnmblALT  25580  limcun  25872  uniin1  32636  uniin2  32637  disjuniel  32682  hashunif  32894  dmvlsiga  34289  measinblem  34380  volmeas  34391  carsggect  34478  omsmeas  34483  tz9.1regs  35294  cvmscld  35471  istotbnd3  38106  sstotbnd  38110  heiborlem3  38148  heibor  38156  limiun  43728  fiunicl  45516  founiiun  45627  founiiun0  45638  psmeasurelem  46916