Theorem uniiun 5081

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

Syntax hints:   = wceq 1537  {cab 2717  ∃wrex 3076  ∪ cuni 4931  ∪ ciun 5015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-rex 3077  df-uni 4932  df-iun 5017

This theorem is referenced by:  iununi  5122  iunpwss  5130  truni  5299  reluni  5842  rnuni  6180  imauni  7283  iunpw  7806  oa0r  8594  om1r  8599  oeworde  8649  unifi  9412  infssuni  9414  cfslb2n  10337  ituniiun  10491  unidom  10612  unictb  10644  gruuni  10869  gruun  10875  hashuni  15874  tgidm  23008  unicld  23075  clsval2  23079  mretopd  23121  tgrest  23188  cmpsublem  23428  cmpsub  23429  tgcmp  23430  hauscmplem  23435  cmpfi  23437  unconn  23458  conncompconn  23461  comppfsc  23561  kgentopon  23567  txbasval  23635  txtube  23669  txcmplem1  23670  txcmplem2  23671  xkococnlem  23688  alexsublem  24073  alexsubALT  24080  opnmblALT  25657  limcun  25950  uniin1  32574  uniin2  32575  disjuniel  32619  hashunif  32813  dmvlsiga  34093  measinblem  34184  volmeas  34195  carsggect  34283  omsmeas  34288  cvmscld  35241  istotbnd3  37731  sstotbnd  37735  heiborlem3  37773  heibor  37781  limiun  43244  fiunicl  44969  founiiun  45086  founiiun0  45097  psmeasurelem  46391