Theorem uniiun 4945

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

Syntax hints:   = wceq 1538  {cab 2776  ∃wrex 3107  ∪ cuni 4800  ∪ ciun 4881

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 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-rex 3112  df-uni 4801  df-iun 4883

This theorem is referenced by:  iununi  4984  iunpwss  4992  truni  5150  reluni  5655  rnuni  5974  imauni  6983  iunpw  7473  oa0r  8146  om1r  8152  oeworde  8202  unifi  8797  infssuni  8799  cfslb2n  9679  ituniiun  9833  unidom  9954  unictb  9986  gruuni  10211  gruun  10217  hashuni  15173  tgidm  21585  unicld  21651  clsval2  21655  mretopd  21697  tgrest  21764  cmpsublem  22004  cmpsub  22005  tgcmp  22006  hauscmplem  22011  cmpfi  22013  unconn  22034  conncompconn  22037  comppfsc  22137  kgentopon  22143  txbasval  22211  txtube  22245  txcmplem1  22246  txcmplem2  22247  xkococnlem  22264  alexsublem  22649  alexsubALT  22656  opnmblALT  24207  limcun  24498  uniin1  30315  uniin2  30316  disjuniel  30360  hashunif  30554  dmvlsiga  31498  measinblem  31589  volmeas  31600  carsggect  31686  omsmeas  31691  cvmscld  32633  istotbnd3  35209  sstotbnd  35213  heiborlem3  35251  heibor  35259  fiunicl  41701  founiiun  41803  founiiun0  41817  psmeasurelem  43109