Theorem uniiun 5024

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

Syntax hints:   = wceq 1567  {cab 2747  ∃wrex 3095  ∪ cuni 4873  ∪ ciun 4957

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-rex 3096  df-uni 4874  df-iun 4959

This theorem is referenced by:  uniin1  5040  uniin2  5041  iununi  5066  iunpwss  5074  truni  5235  reluni  5803  rnuni  6144  imauni  7242  iunpw  7766  oa0r  8519  om1r  8524  oeworde  8575  unifi  9297  infssuni  9299  cfslb2n  10248  ituniiun  10402  unidom  10523  unictb  10556  gruuni  10781  gruun  10787  hashuni  15874  tgidm  23102  unicld  23168  clsval2  23172  mretopd  23214  tgrest  23281  cmpsublem  23521  cmpsub  23522  tgcmp  23523  hauscmplem  23528  cmpfi  23530  unconn  23551  conncompconn  23554  comppfsc  23654  kgentopon  23660  txbasval  23728  txtube  23762  txcmplem1  23763  txcmplem2  23764  xkococnlem  23781  alexsublem  24166  alexsubALT  24173  opnmblALT  25727  limcun  26019  disjuniel  32879  hashunif  33088  dmvlsiga  34460  measinblem  34551  volmeas  34562  carsggect  34649  omsmeas  34654  tz9.1regs  35466  cvmscld  35660  istotbnd3  38305  sstotbnd  38309  heiborlem3  38347  heibor  38355  limiun  43894  fiunicl  45672  founiiun  45782  founiiun0  45793  psmeasurelem  47069