![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > uniiun | Structured version Visualization version GIF version |
Description: Class union in terms of indexed union. Definition in [Stoll] p. 43. (Contributed by NM, 28-Jun-1998.) |
Ref | Expression |
---|---|
uniiun | ⊢ ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝑥 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfuni2 4675 | . 2 ⊢ ∪ 𝐴 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝑥} | |
2 | df-iun 4757 | . 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝑥 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝑥} | |
3 | 1, 2 | eqtr4i 2805 | 1 ⊢ ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝑥 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1601 {cab 2763 ∃wrex 3091 ∪ cuni 4673 ∪ ciun 4755 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-tru 1605 df-ex 1824 df-sb 2012 df-clab 2764 df-cleq 2770 df-rex 3096 df-uni 4674 df-iun 4757 |
This theorem is referenced by: iununi 4846 iunpwss 4854 truni 5003 reluni 5491 rnuni 5800 imauni 6778 iunpw 7258 oa0r 7904 om1r 7909 oeworde 7959 unifi 8545 infssuni 8547 cfslb2n 9427 ituniiun 9581 unidom 9702 unictb 9734 gruuni 9959 gruun 9965 hashuni 14966 tgidm 21196 unicld 21262 clsval2 21266 mretopd 21308 tgrest 21375 cmpsublem 21615 cmpsub 21616 tgcmp 21617 hauscmplem 21622 cmpfi 21624 unconn 21645 conncompconn 21648 comppfsc 21748 kgentopon 21754 txbasval 21822 txtube 21856 txcmplem1 21857 txcmplem2 21858 xkococnlem 21875 alexsublem 22260 alexsubALT 22267 opnmblALT 23811 limcun 24100 uniin1 29934 uniin2 29935 disjuniel 29977 hashunif 30130 dmvlsiga 30794 measinblem 30885 volmeas 30896 carsggect 30982 omsmeas 30987 cvmscld 31858 istotbnd3 34199 sstotbnd 34203 heiborlem3 34241 heibor 34249 fiunicl 40177 founiiun 40294 founiiun0 40310 psmeasurelem 41621 |
Copyright terms: Public domain | W3C validator |