Theorem uniiun 5022

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

This proof depends on syntax axioms:   = wceq 1570  {cab 2741  ∃wrex 3090  ∪ cuni 4872  ∪ ciun 4956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-rex 3091  df-uni 4873  df-iun 4958

This theorem is used by:  uniin1  5038  uniin2  5039  iununi  5064  iunpwss  5072  truni  5234  reluni  5805  rnuni  6158  imauni  7281  iunpw  7817  oa0r  8584  om1r  8589  oeworde  8640  unifi  9371  infssuni  9373  cfslb2n  10385  ituniiun  10539  unidom  10666  unictb  10699  gruuni  10924  gruun  10930  hashuni  16037  tgidm  23353  unicld  23419  clsval2  23423  mretopd  23465  tgrest  23532  cmpsublem  23772  cmpsub  23773  tgcmp  23774  hauscmplem  23779  cmpfi  23781  unconn  23802  conncompconn  23805  comppfsc  23906  kgentopon  23912  txbasval  23980  txtube  24014  txcmplem1  24015  txcmplem2  24016  xkococnlem  24033  alexsublem  24418  alexsubALT  24425  opnmblALT  25979  limcun  26270  disjuniel  33289  hashunif  33494  dmvlsiga  34872  measinblem  34964  volmeas  34975  carsggect  35061  omsmeas  35066  tz9.1regs  35943  cvmscld  36246  istotbnd3  38971  sstotbnd  38975  heiborlem3  39013  heibor  39021  limiun  44545  fiunicl  46358  founiiun  46467  founiiun0  46478  psmeasurelem  47753