| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > dfiun2 | Structured version Visualization version GIF version | ||
| Description: Alternate definition of indexed union when 𝐵 is a set. Definition 15(a) of [Suppes] p. 44. (Contributed by NM, 27-Jun-1998.) (Revised by David Abernethy, 19-Jun-2012.) |
| Ref | Expression |
|---|---|
| dfiun2.1 | ⊢ 𝐵 ∈ V |
| Ref | Expression |
|---|---|
| dfiun2 | ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfiun2g 5030 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ V → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) | |
| 2 | dfiun2.1 | . . 3 ⊢ 𝐵 ∈ V | |
| 3 | 2 | a1i 11 | . 2 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ∈ V) |
| 4 | 1, 3 | mprg 3067 | 1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 ∈ wcel 2108 {cab 2714 ∃wrex 3070 Vcvv 3480 ∪ cuni 4907 ∪ 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-11 2157 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-uni 4908 df-iun 4993 |
| This theorem is referenced by: fniunfv 7267 funcnvuni 7954 fiun 7967 f1iun 7968 tfrlem8 8424 rdglim2a 8473 rankuni 9903 cardiun 10022 kmlem11 10201 cfslb2n 10308 enfin2i 10361 pwcfsdom 10623 rankcf 10817 tskuni 10823 discmp 23406 cmpsublem 23407 cmpsub 23408 nnoeomeqom 43325 |
| Copyright terms: Public domain | W3C validator |