Theorem uniiun 5062

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

Syntax hints:   = wceq 1536  {cab 2711  ∃wrex 3067  ∪ cuni 4911  ∪ ciun 4995

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-rex 3068  df-uni 4912  df-iun 4997

This theorem is referenced by:  iununi  5103  iunpwss  5111  truni  5280  reluni  5830  rnuni  6170  imauni  7265  iunpw  7789  oa0r  8574  om1r  8579  oeworde  8629  unifi  9381  infssuni  9383  cfslb2n  10305  ituniiun  10459  unidom  10580  unictb  10612  gruuni  10837  gruun  10843  hashuni  15858  tgidm  23002  unicld  23069  clsval2  23073  mretopd  23115  tgrest  23182  cmpsublem  23422  cmpsub  23423  tgcmp  23424  hauscmplem  23429  cmpfi  23431  unconn  23452  conncompconn  23455  comppfsc  23555  kgentopon  23561  txbasval  23629  txtube  23663  txcmplem1  23664  txcmplem2  23665  xkococnlem  23682  alexsublem  24067  alexsubALT  24074  opnmblALT  25651  limcun  25944  uniin1  32571  uniin2  32572  disjuniel  32616  hashunif  32815  dmvlsiga  34109  measinblem  34200  volmeas  34211  carsggect  34299  omsmeas  34304  cvmscld  35257  istotbnd3  37757  sstotbnd  37761  heiborlem3  37799  heibor  37807  limiun  43271  fiunicl  45006  founiiun  45121  founiiun0  45132  psmeasurelem  46425