Theorem uniiun 4573

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

Syntax hints:   = wceq 1483  {cab 2608  ∃wrex 2913  ∪ cuni 4436  ∪ ciun 4520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-rex 2918  df-uni 4437  df-iun 4522

This theorem is referenced by:  iununi  4610  iunpwss  4618  truni  4767  reluni  5241  rnuni  5544  imauni  6504  iunpw  6978  oa0r  7618  om1r  7623  oeworde  7673  unifi  8255  infssuni  8257  cfslb2n  9090  ituniiun  9244  unidom  9365  unictb  9397  gruuni  9622  gruun  9628  hashuni  14558  tgidm  20784  unicld  20850  clsval2  20854  mretopd  20896  tgrest  20963  cmpsublem  21202  cmpsub  21203  tgcmp  21204  hauscmplem  21209  cmpfi  21211  unconn  21232  conncompconn  21235  comppfsc  21335  kgentopon  21341  txbasval  21409  txtube  21443  txcmplem1  21444  txcmplem2  21445  xkococnlem  21462  alexsublem  21848  alexsubALT  21855  opnmblALT  23371  limcun  23659  uniin1  29367  uniin2  29368  disjuniel  29410  hashunif  29562  dmvlsiga  30192  measinblem  30283  volmeas  30294  carsggect  30380  omsmeas  30385  cvmscld  31255  istotbnd3  33570  sstotbnd  33574  heiborlem3  33612  heibor  33620  fiunicl  39236  founiiun  39360  founiiun0  39377  psmeasurelem  40687