![]() |
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 4914 | . 2 ⊢ ∪ 𝐴 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝑥} | |
2 | df-iun 5002 | . 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝑥 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝑥} | |
3 | 1, 2 | eqtr4i 2756 | 1 ⊢ ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝑥 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1533 {cab 2702 ∃wrex 3059 ∪ cuni 4912 ∪ ciun 5000 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-rex 3060 df-uni 4913 df-iun 5002 |
This theorem is referenced by: iununi 5106 iunpwss 5114 truni 5285 reluni 5823 rnuni 6159 imauni 7260 iunpw 7778 oa0r 8567 om1r 8572 oeworde 8622 unifi 9381 infssuni 9383 cfslb2n 10307 ituniiun 10461 unidom 10582 unictb 10614 gruuni 10839 gruun 10845 hashuni 15825 tgidm 22966 unicld 23033 clsval2 23037 mretopd 23079 tgrest 23146 cmpsublem 23386 cmpsub 23387 tgcmp 23388 hauscmplem 23393 cmpfi 23395 unconn 23416 conncompconn 23419 comppfsc 23519 kgentopon 23525 txbasval 23593 txtube 23627 txcmplem1 23628 txcmplem2 23629 xkococnlem 23646 alexsublem 24031 alexsubALT 24038 opnmblALT 25615 limcun 25907 uniin1 32463 uniin2 32464 disjuniel 32508 hashunif 32699 dmvlsiga 33918 measinblem 34009 volmeas 34020 carsggect 34108 omsmeas 34113 cvmscld 35053 istotbnd3 37420 sstotbnd 37424 heiborlem3 37462 heibor 37470 limiun 42885 fiunicl 44605 founiiun 44723 founiiun0 44734 psmeasurelem 46028 |
Copyright terms: Public domain | W3C validator |