Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > iuneq2d | Structured version Visualization version Unicode version |
Description: Equality deduction for indexed union. (Contributed by Drahflow, 22-Oct-2015.) |
Ref | Expression |
---|---|
iuneq2d.2 |
Ref | Expression |
---|---|
iuneq2d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iuneq2d.2 | . . 3 | |
2 | 1 | adantr 481 | . 2 |
3 | 2 | iuneq2dv 4542 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wceq 1483 wcel 1990 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: iununi 4610 oelim2 7675 ituniiun 9244 dfrtrclrec2 13797 rtrclreclem1 13798 rtrclreclem2 13799 rtrclreclem4 13801 imasval 16171 mreacs 16319 cnextval 21865 taylfval 24113 iunpreima 29383 reprdifc 30705 msubvrs 31457 trpredeq1 31720 trpredeq2 31721 neibastop2 32356 voliunnfl 33453 sstotbnd2 33573 equivtotbnd 33577 totbndbnd 33588 heiborlem3 33612 eliunov2 37971 fvmptiunrelexplb0d 37976 fvmptiunrelexplb1d 37978 comptiunov2i 37998 trclrelexplem 38003 dftrcl3 38012 trclfvcom 38015 cnvtrclfv 38016 cotrcltrcl 38017 trclimalb2 38018 trclfvdecomr 38020 dfrtrcl3 38025 dfrtrcl4 38030 isomenndlem 40744 ovnval 40755 hoicvr 40762 hoicvrrex 40770 ovnlecvr 40772 ovncvrrp 40778 ovnsubaddlem1 40784 hoidmvlelem3 40811 hoidmvle 40814 ovnhoilem1 40815 ovnovollem1 40870 smflimlem3 40981 otiunsndisjX 41298 |
Copyright terms: Public domain | W3C validator |