| 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 5090 | . 2 ⊢ (𝐴 ∈ V → ∪ 𝑥 ∈ {𝐴}𝐵 = 𝐶) |
| 4 | 1, 3 | ax-mp 5 | 1 ⊢ ∪ 𝑥 ∈ {𝐴}𝐵 = 𝐶 |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2108 Vcvv 3480 {csn 4626 ∪ ciun 4991 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-rex 3071 df-v 3482 df-sn 4627 df-iun 4993 |
| This theorem is referenced by: iunsuc 6469 funopsn 7168 fparlem3 8139 fparlem4 8140 iunfi 9383 kmlem11 10201 ackbij1lem8 10266 dfid6 15067 fsum2dlem 15806 fsumiun 15857 fprod2dlem 16016 prmreclem4 16957 fiuncmp 23412 ovolfiniun 25536 finiunmbl 25579 volfiniun 25582 voliunlem1 25585 iuninc 32573 cvmliftlem10 35299 mrsubvrs 35527 dfrcl4 43689 iunrelexp0 43715 corclrcl 43720 cotrcltrcl 43738 trclfvdecomr 43741 dfrtrcl4 43751 corcltrcl 43752 cotrclrcl 43755 |
| Copyright terms: Public domain | W3C validator |