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 4960 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) | |
2 | 1 | adantl 482 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) |
3 | abrexexg 7803 | . . . 4 ⊢ (𝐴 ∈ 𝑉 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V) | |
4 | 3 | uniexd 7595 | . . 3 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V) |
5 | 4 | adantr 481 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V) |
6 | 2, 5 | eqeltrd 2839 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1539 ∈ wcel 2106 {cab 2715 ∀wral 3064 ∃wrex 3065 Vcvv 3432 ∪ cuni 4839 ∪ ciun 4924 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-11 2154 ax-ext 2709 ax-rep 5209 ax-sep 5223 ax-un 7588 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1542 df-ex 1783 df-sb 2068 df-mo 2540 df-clab 2716 df-cleq 2730 df-clel 2816 df-ral 3069 df-rex 3070 df-v 3434 df-in 3894 df-ss 3904 df-uni 4840 df-iun 4926 |
This theorem is referenced by: abrexex2g 7807 opabex3d 7808 opabex3rd 7809 opabex3 7810 iunex 7811 xpexgALT 7824 mpoexxg 7916 ixpexg 8710 ixpssmapg 8716 ttrclselem2 9484 iundom 10298 iunctb 10330 wrdexg 14227 cshwsex 16802 imasplusg 17228 imasmulr 17229 imasvsca 17231 imasip 17232 gsum2d2 19575 gsumcom2 19576 dprd2da 19645 ptcls 22767 ptcmplem2 23204 elpwiuncl 30876 aciunf1lem 30999 gsumpart 31315 esum2dlem 32060 esum2d 32061 esumiun 32062 omssubadd 32267 eulerpartlemgs2 32347 bnj535 32870 bnj546 32876 bnj893 32908 bnj1136 32977 bnj1413 33015 eliunov2 41287 fvmptiunrelexplb0d 41292 fvmptiunrelexplb1d 41294 iunrelexp0 41310 collexd 41875 unirnmapsn 42754 iunmapss 42755 ssmapsn 42756 iunmapsn 42757 sge0iunmptlemfi 43951 sge0iunmpt 43956 smflimlem1 44306 smfliminflem 44363 mpoexxg2 45673 |
Copyright terms: Public domain | W3C validator |