| 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 4909 | . 2 ⊢ ∪ 𝐴 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝑥} | |
| 2 | df-iun 4993 | . 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝑥 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝑥} | |
| 3 | 1, 2 | eqtr4i 2768 | 1 ⊢ ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝑥 |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 {cab 2714 ∃wrex 3070 ∪ cuni 4907 ∪ ciun 4991 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-rex 3071 df-uni 4908 df-iun 4993 |
| This theorem is referenced by: iununi 5099 iunpwss 5107 truni 5275 reluni 5828 rnuni 6168 imauni 7266 iunpw 7791 oa0r 8576 om1r 8581 oeworde 8631 unifi 9384 infssuni 9386 cfslb2n 10308 ituniiun 10462 unidom 10583 unictb 10615 gruuni 10840 gruun 10846 hashuni 15862 tgidm 22987 unicld 23054 clsval2 23058 mretopd 23100 tgrest 23167 cmpsublem 23407 cmpsub 23408 tgcmp 23409 hauscmplem 23414 cmpfi 23416 unconn 23437 conncompconn 23440 comppfsc 23540 kgentopon 23546 txbasval 23614 txtube 23648 txcmplem1 23649 txcmplem2 23650 xkococnlem 23667 alexsublem 24052 alexsubALT 24059 opnmblALT 25638 limcun 25930 uniin1 32564 uniin2 32565 disjuniel 32610 hashunif 32810 dmvlsiga 34130 measinblem 34221 volmeas 34232 carsggect 34320 omsmeas 34325 cvmscld 35278 istotbnd3 37778 sstotbnd 37782 heiborlem3 37820 heibor 37828 limiun 43295 fiunicl 45072 founiiun 45184 founiiun0 45195 psmeasurelem 46485 |
| Copyright terms: Public domain | W3C validator |