Theorem uniiun 5001

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

Syntax hints:   = wceq 1542  {cab 2714  ∃wrex 3061  ∪ cuni 4850  ∪ ciun 4933

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-rex 3062  df-uni 4851  df-iun 4935

This theorem is referenced by:  iununi  5041  iunpwss  5049  truni  5208  reluni  5774  rnuni  6112  imauni  7201  iunpw  7725  oa0r  8473  om1r  8478  oeworde  8529  unifi  9254  infssuni  9256  cfslb2n  10190  ituniiun  10344  unidom  10465  unictb  10498  gruuni  10723  gruun  10729  hashuni  15789  tgidm  22945  unicld  23011  clsval2  23015  mretopd  23057  tgrest  23124  cmpsublem  23364  cmpsub  23365  tgcmp  23366  hauscmplem  23371  cmpfi  23373  unconn  23394  conncompconn  23397  comppfsc  23497  kgentopon  23503  txbasval  23571  txtube  23605  txcmplem1  23606  txcmplem2  23607  xkococnlem  23624  alexsublem  24009  alexsubALT  24016  opnmblALT  25570  limcun  25862  uniin1  32621  uniin2  32622  disjuniel  32667  hashunif  32879  dmvlsiga  34273  measinblem  34364  volmeas  34375  carsggect  34462  omsmeas  34467  tz9.1regs  35278  cvmscld  35455  istotbnd3  38092  sstotbnd  38096  heiborlem3  38134  heibor  38142  limiun  43710  fiunicl  45498  founiiun  45609  founiiun0  45620  psmeasurelem  46898