| 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 4997 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) | |
| 2 | 1 | adantl 481 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) |
| 3 | abrexexg 7942 | . . . 4 ⊢ (𝐴 ∈ 𝑉 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V) | |
| 4 | 3 | uniexd 7721 | . . 3 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V) |
| 5 | 4 | adantr 480 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V) |
| 6 | 2, 5 | eqeltrd 2829 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2109 {cab 2708 ∀wral 3045 ∃wrex 3054 Vcvv 3450 ∪ cuni 4874 ∪ ciun 4958 |
| 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-11 2158 ax-ext 2702 ax-rep 5237 ax-sep 5254 ax-un 7714 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2066 df-mo 2534 df-clab 2709 df-cleq 2722 df-clel 2804 df-ral 3046 df-rex 3055 df-v 3452 df-ss 3934 df-uni 4875 df-iun 4960 |
| This theorem is referenced by: abrexex2g 7946 opabex3d 7947 opabex3rd 7948 opabex3 7949 iunex 7950 xpexgALT 7963 mpoexxg 8057 ixpexg 8898 ixpssmapg 8904 ttrclselem2 9686 iundom 10502 iunctb 10534 wrdexg 14496 cshwsex 17078 imasplusg 17487 imasmulr 17488 imasvsca 17490 imasip 17491 gsum2d2 19911 gsumcom2 19912 dprd2da 19981 ptcls 23510 ptcmplem2 23947 elpwiuncl 32463 aciunf1lem 32593 gsumpart 33004 gsumwrd2dccat 33014 irngval 33687 esum2dlem 34089 esum2d 34090 esumiun 34091 omssubadd 34298 eulerpartlemgs2 34378 bnj535 34887 bnj546 34893 bnj893 34925 bnj1136 34994 bnj1413 35032 weiunse 36463 numiunnum 36465 eliunov2 43675 fvmptiunrelexplb0d 43680 fvmptiunrelexplb1d 43682 iunrelexp0 43698 collexd 44253 unirnmapsn 45215 iunmapss 45216 ssmapsn 45217 iunmapsn 45218 sge0iunmptlemfi 46418 sge0iunmpt 46423 smflimlem1 46776 smfliminflem 46835 mpoexxg2 48330 imasubclem1 49097 |
| Copyright terms: Public domain | W3C validator |