Theorem uniiun 4988

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 4923	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝑥 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝑥}
3	1, 2	eqtr4i 2765	1 ⊢ ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝑥

Syntax hints:   = wceq 1547  {cab 2717  ∃wrex 3063  ∪ cuni 4838  ∪ ciun 4921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-rex 3064  df-uni 4839  df-iun 4923

This theorem is referenced by:  iununi  5028  iunpwss  5036  truni  5195  reluni  5761  rnuni  6099  imauni  7190  iunpw  7714  oa0r  8463  om1r  8468  oeworde  8519  unifi  9244  infssuni  9246  cfslb2n  10181  ituniiun  10335  unidom  10456  unictb  10489  gruuni  10714  gruun  10720  hashuni  15780  tgidm  22963  unicld  23029  clsval2  23033  mretopd  23075  tgrest  23142  cmpsublem  23382  cmpsub  23383  tgcmp  23384  hauscmplem  23389  cmpfi  23391  unconn  23412  conncompconn  23415  comppfsc  23515  kgentopon  23521  txbasval  23589  txtube  23623  txcmplem1  23624  txcmplem2  23625  xkococnlem  23642  alexsublem  24027  alexsubALT  24034  opnmblALT  25588  limcun  25880  uniin1  32640  uniin2  32641  disjuniel  32686  hashunif  32898  dmvlsiga  34313  measinblem  34404  volmeas  34415  carsggect  34502  omsmeas  34507  tz9.1regs  35315  cvmscld  35501  istotbnd3  38138  sstotbnd  38142  heiborlem3  38180  heibor  38188  limiun  43727  fiunicl  45515  founiiun  45626  founiiun0  45637  psmeasurelem  46913