![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > iuneq2i | Structured version Visualization version Unicode version |
Description: Equality inference for indexed union. (Contributed by NM, 22-Oct-2003.) |
Ref | Expression |
---|---|
iuneq2i.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
iuneq2i |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iuneq2 4308 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | iuneq2i.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mprg 2762 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 |
This theorem depends on definitions: df-bi 190 df-an 377 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2591 df-ral 2753 df-rex 2754 df-v 3058 df-in 3422 df-ss 3429 df-iun 4293 |
This theorem is referenced by: dfiunv2 4327 iunrab 4338 iunid 4346 iunin1 4356 2iunin 4359 resiun1 5141 resiun2 5142 dfimafn2 5937 dfmpt 6092 funiunfv 6177 fpar 6926 onovuni 7086 uniqs 7448 marypha2lem2 7975 alephlim 8523 cfsmolem 8725 ituniiun 8877 imasdsval2 15465 imasdsval2OLD 15477 lpival 18517 cmpsublem 20462 txbasval 20669 uniioombllem2 22588 uniioombllem2OLD 22589 uniioombllem4 22592 volsup2 22611 itg1addlem5 22706 itg1climres 22720 indval2 28884 sigaclfu2 28991 measvuni 29084 trpred0 30525 rabiun 31970 mblfinlem2 32022 voliunnfl 32028 cnambfre 32033 trclrelexplem 36347 cotrclrcl 36378 hoicvr 38407 hoidmv1le 38453 hoidmvle 38459 hspmbllem2 38486 dfaimafn2 38705 xpiun 40038 |
Copyright terms: Public domain | W3C validator |