Theorem uniiun 5017

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

This proof depends on syntax axioms:   = wceq 1570  {cab 2738  ∃wrex 3086  ∪ cuni 4867  ∪ ciun 4951

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-rex 3087  df-uni 4868  df-iun 4953

This theorem is used by:  uniin1  5033  uniin2  5034  iununi  5059  iunpwss  5067  truni  5228  reluni  5799  rnuni  6140  imauni  7243  iunpw  7770  oa0r  8525  om1r  8530  oeworde  8581  unifi  9311  infssuni  9313  cfslb2n  10270  ituniiun  10424  unidom  10551  unictb  10584  gruuni  10809  gruun  10815  hashuni  15913  tgidm  23205  unicld  23271  clsval2  23275  mretopd  23317  tgrest  23384  cmpsublem  23624  cmpsub  23625  tgcmp  23626  hauscmplem  23631  cmpfi  23633  unconn  23654  conncompconn  23657  comppfsc  23758  kgentopon  23764  txbasval  23832  txtube  23866  txcmplem1  23867  txcmplem2  23868  xkococnlem  23885  alexsublem  24270  alexsubALT  24277  opnmblALT  25831  limcun  26122  disjuniel  33070  hashunif  33277  dmvlsiga  34639  measinblem  34731  volmeas  34742  carsggect  34829  omsmeas  34834  tz9.1regs  35660  cvmscld  35852  istotbnd3  38521  sstotbnd  38525  heiborlem3  38563  heibor  38571  limiun  44123  fiunicl  45901  founiiun  46011  founiiun0  46022  psmeasurelem  47298