![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > iunxsn | Structured version Visualization version GIF 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 | ⊢ 𝐴 ∈ V |
iunxsn.2 | ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) |
Ref | Expression |
---|---|
iunxsn | ⊢ ∪ 𝑥 ∈ {𝐴}𝐵 = 𝐶 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iunxsn.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | iunxsn.2 | . . 3 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) | |
3 | 2 | iunxsng 4791 | . 2 ⊢ (𝐴 ∈ V → ∪ 𝑥 ∈ {𝐴}𝐵 = 𝐶) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ ∪ 𝑥 ∈ {𝐴}𝐵 = 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1653 ∈ wcel 2157 Vcvv 3384 {csn 4367 ∪ ciun 4709 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-ext 2776 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2785 df-cleq 2791 df-clel 2794 df-nfc 2929 df-ral 3093 df-rex 3094 df-v 3386 df-sbc 3633 df-sn 4368 df-iun 4711 |
This theorem is referenced by: iunsuc 6022 funopsn 6640 fparlem3 7515 fparlem4 7516 iunfi 8495 kmlem11 9269 ackbij1lem8 9336 dfid6 14106 fsum2dlem 14837 fsumiun 14888 fprod2dlem 15044 prmreclem4 15953 fiuncmp 21533 ovolfiniun 23606 finiunmbl 23649 volfiniun 23652 voliunlem1 23655 iuninc 29889 cvmliftlem10 31786 mrsubvrs 31929 dfrcl4 38740 iunrelexp0 38766 corclrcl 38771 cotrcltrcl 38789 trclfvdecomr 38792 dfrtrcl4 38802 corcltrcl 38803 cotrclrcl 38806 |
Copyright terms: Public domain | W3C validator |