Theorem uniiun 4982

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

Syntax hints:   = wceq 1537  {cab 2799  ∃wrex 3139  ∪ cuni 4838  ∪ ciun 4919

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2800  df-cleq 2814  df-rex 3144  df-uni 4839  df-iun 4921

This theorem is referenced by:  iununi  5021  iunpwss  5029  truni  5186  reluni  5691  rnuni  6007  imauni  7005  iunpw  7493  oa0r  8163  om1r  8169  oeworde  8219  unifi  8813  infssuni  8815  cfslb2n  9690  ituniiun  9844  unidom  9965  unictb  9997  gruuni  10222  gruun  10228  hashuni  15181  tgidm  21588  unicld  21654  clsval2  21658  mretopd  21700  tgrest  21767  cmpsublem  22007  cmpsub  22008  tgcmp  22009  hauscmplem  22014  cmpfi  22016  unconn  22037  conncompconn  22040  comppfsc  22140  kgentopon  22146  txbasval  22214  txtube  22248  txcmplem1  22249  txcmplem2  22250  xkococnlem  22267  alexsublem  22652  alexsubALT  22659  opnmblALT  24204  limcun  24493  uniin1  30303  uniin2  30304  disjuniel  30347  hashunif  30528  dmvlsiga  31388  measinblem  31479  volmeas  31490  carsggect  31576  omsmeas  31581  cvmscld  32520  istotbnd3  35064  sstotbnd  35068  heiborlem3  35106  heibor  35114  fiunicl  41378  founiiun  41484  founiiun0  41500  psmeasurelem  42801