Theorem uniiun 4984

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

Syntax hints:   = wceq 1539  {cab 2715  ∃wrex 3064  ∪ cuni 4836  ∪ ciun 4921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-rex 3069  df-uni 4837  df-iun 4923

This theorem is referenced by:  iununi  5024  iunpwss  5032  truni  5201  reluni  5717  rnuni  6041  imauni  7101  iunpw  7599  oa0r  8330  om1r  8336  oeworde  8386  unifi  9038  infssuni  9040  cfslb2n  9955  ituniiun  10109  unidom  10230  unictb  10262  gruuni  10487  gruun  10493  hashuni  15466  tgidm  22038  unicld  22105  clsval2  22109  mretopd  22151  tgrest  22218  cmpsublem  22458  cmpsub  22459  tgcmp  22460  hauscmplem  22465  cmpfi  22467  unconn  22488  conncompconn  22491  comppfsc  22591  kgentopon  22597  txbasval  22665  txtube  22699  txcmplem1  22700  txcmplem2  22701  xkococnlem  22718  alexsublem  23103  alexsubALT  23110  opnmblALT  24672  limcun  24964  uniin1  30792  uniin2  30793  disjuniel  30837  hashunif  31028  dmvlsiga  31997  measinblem  32088  volmeas  32099  carsggect  32185  omsmeas  32190  cvmscld  33135  istotbnd3  35856  sstotbnd  35860  heiborlem3  35898  heibor  35906  fiunicl  42504  founiiun  42604  founiiun0  42617  psmeasurelem  43898