| 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 5049 | . 2 ⊢ (𝐴 ∈ V → ∪ 𝑥 ∈ {𝐴}𝐵 = 𝐶) |
| 4 | 1, 3 | ax-mp 5 | 1 ⊢ ∪ 𝑥 ∈ {𝐴}𝐵 = 𝐶 |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2109 Vcvv 3444 {csn 4585 ∪ ciun 4951 |
| 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 2008 ax-8 2111 ax-9 2119 ax-ext 2701 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2721 df-clel 2803 df-ral 3045 df-rex 3054 df-v 3446 df-sn 4586 df-iun 4953 |
| This theorem is referenced by: iunsuc 6407 funopsn 7102 fparlem3 8070 fparlem4 8071 iunfi 9270 kmlem11 10092 ackbij1lem8 10157 dfid6 14971 fsum2dlem 15713 fsumiun 15764 fprod2dlem 15923 prmreclem4 16867 fiuncmp 23325 ovolfiniun 25436 finiunmbl 25479 volfiniun 25482 voliunlem1 25485 iuninc 32540 cvmliftlem10 35275 mrsubvrs 35503 dfrcl4 43659 iunrelexp0 43685 corclrcl 43690 cotrcltrcl 43708 trclfvdecomr 43711 dfrtrcl4 43721 corcltrcl 43722 cotrclrcl 43725 imaf1hom 49091 |
| Copyright terms: Public domain | W3C validator |