Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > iuneq1 | Structured version Visualization version Unicode version |
Description: Equality theorem for indexed union. (Contributed by NM, 27-Jun-1998.) |
Ref | Expression |
---|---|
iuneq1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iunss1 4532 | . . 3 | |
2 | iunss1 4532 | . . 3 | |
3 | 1, 2 | anim12i 590 | . 2 |
4 | eqss 3618 | . 2 | |
5 | eqss 3618 | . 2 | |
6 | 3, 4, 5 | 3imtr4i 281 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 wceq 1483 wss 3574 ciun 4520 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ral 2917 df-rex 2918 df-v 3202 df-in 3581 df-ss 3588 df-iun 4522 |
This theorem is referenced by: iuneq1d 4545 iinvdif 4592 iunxprg 4607 iununi 4610 iunsuc 5807 funopsn 6413 funiunfv 6506 onfununi 7438 iunfi 8254 rankuni2b 8716 pwsdompw 9026 ackbij1lem7 9048 r1om 9066 fictb 9067 cfsmolem 9092 ituniiun 9244 domtriomlem 9264 domtriom 9265 inar1 9597 fsum2d 14502 fsumiun 14553 ackbijnn 14560 fprod2d 14711 prmreclem5 15624 lpival 19245 fiuncmp 21207 ovolfiniun 23269 ovoliunnul 23275 finiunmbl 23312 volfiniun 23315 voliunlem1 23318 iuninc 29379 ofpreima2 29466 esum2dlem 30154 sigaclfu2 30184 sigapildsyslem 30224 fiunelros 30237 bnj548 30967 bnj554 30969 bnj594 30982 trpredlem1 31727 trpredtr 31730 trpredmintr 31731 trpredrec 31738 neibastop2lem 32355 istotbnd3 33570 0totbnd 33572 sstotbnd2 33573 sstotbnd 33574 sstotbnd3 33575 totbndbnd 33588 prdstotbnd 33593 cntotbnd 33595 heibor 33620 dfrcl4 37968 iunrelexp0 37994 comptiunov2i 37998 corclrcl 37999 cotrcltrcl 38017 trclfvdecomr 38020 dfrtrcl4 38030 corcltrcl 38031 cotrclrcl 38034 fiiuncl 39234 iuneq1i 39259 sge0iunmptlemfi 40630 caragenfiiuncl 40729 carageniuncllem1 40735 ovnsubadd2lem 40859 |
Copyright terms: Public domain | W3C validator |