![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > iunxsn | Structured version Visualization version Unicode version |
Description: A singleton index picks out an instance of an indexed union's argument. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Mario Carneiro, 25-Jun-2016.) |
Ref | Expression |
---|---|
iunxsn.1 |
![]() ![]() ![]() ![]() |
iunxsn.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
iunxsn |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iunxsn.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | iunxsn.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | iunxsng 4374 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | ax-mp 5 |
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 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-an 377 df-3an 993 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ral 2754 df-rex 2755 df-v 3059 df-sbc 3280 df-sn 3981 df-iun 4294 |
This theorem is referenced by: iunsuc 5528 fparlem3 6930 fparlem4 6931 iunfi 7893 kmlem11 8621 ackbij1lem8 8688 dfid6 13146 fsum2dlem 13886 fsumiun 13936 fprod2dlem 14089 prmreclem4 14918 fiuncmp 20474 ovolfiniun 22509 finiunmbl 22553 volfiniun 22556 voliunlem1 22559 iuninc 28230 cvmliftlem10 30067 mrsubvrs 30210 dfrcl4 36314 iunrelexp0 36340 corclrcl 36345 cotrcltrcl 36363 trclfvdecomr 36366 dfrtrcl4 36376 corcltrcl 36377 cotrclrcl 36380 funopsn 39156 |
Copyright terms: Public domain | W3C validator |