| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > iunexg | Structured version Visualization version GIF version | ||
| Description: The existence of an indexed union. 𝑥 is normally a free-variable parameter in 𝐵. (Contributed by NM, 23-Mar-2006.) |
| Ref | Expression |
|---|---|
| iunexg | ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfiun2g 5030 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) | |
| 2 | 1 | adantl 481 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) |
| 3 | abrexexg 7985 | . . . 4 ⊢ (𝐴 ∈ 𝑉 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V) | |
| 4 | 3 | uniexd 7762 | . . 3 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V) |
| 5 | 4 | adantr 480 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V) |
| 6 | 2, 5 | eqeltrd 2841 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2108 {cab 2714 ∀wral 3061 ∃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 ax-rep 5279 ax-sep 5296 ax-un 7755 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-mo 2540 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-rex 3071 df-v 3482 df-ss 3968 df-uni 4908 df-iun 4993 |
| This theorem is referenced by: abrexex2g 7989 opabex3d 7990 opabex3rd 7991 opabex3 7992 iunex 7993 xpexgALT 8006 mpoexxg 8100 ixpexg 8962 ixpssmapg 8968 ttrclselem2 9766 iundom 10582 iunctb 10614 wrdexg 14562 cshwsex 17138 imasplusg 17562 imasmulr 17563 imasvsca 17565 imasip 17566 gsum2d2 19992 gsumcom2 19993 dprd2da 20062 ptcls 23624 ptcmplem2 24061 elpwiuncl 32546 aciunf1lem 32672 gsumpart 33060 gsumwrd2dccat 33070 irngval 33735 esum2dlem 34093 esum2d 34094 esumiun 34095 omssubadd 34302 eulerpartlemgs2 34382 bnj535 34904 bnj546 34910 bnj893 34942 bnj1136 35011 bnj1413 35049 weiunse 36469 numiunnum 36471 eliunov2 43692 fvmptiunrelexplb0d 43697 fvmptiunrelexplb1d 43699 iunrelexp0 43715 collexd 44276 unirnmapsn 45219 iunmapss 45220 ssmapsn 45221 iunmapsn 45222 sge0iunmptlemfi 46428 sge0iunmpt 46433 smflimlem1 46786 smfliminflem 46845 mpoexxg2 48254 |
| Copyright terms: Public domain | W3C validator |