![]() |
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 5035 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) | |
2 | 1 | adantl 481 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) |
3 | abrexexg 7984 | . . . 4 ⊢ (𝐴 ∈ 𝑉 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V) | |
4 | 3 | uniexd 7761 | . . 3 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V) |
5 | 4 | adantr 480 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V) |
6 | 2, 5 | eqeltrd 2839 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 = wceq 1537 ∈ wcel 2106 {cab 2712 ∀wral 3059 ∃wrex 3068 Vcvv 3478 ∪ cuni 4912 ∪ ciun 4996 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-11 2155 ax-ext 2706 ax-rep 5285 ax-sep 5302 ax-un 7754 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1540 df-ex 1777 df-sb 2063 df-mo 2538 df-clab 2713 df-cleq 2727 df-clel 2814 df-ral 3060 df-rex 3069 df-v 3480 df-ss 3980 df-uni 4913 df-iun 4998 |
This theorem is referenced by: abrexex2g 7988 opabex3d 7989 opabex3rd 7990 opabex3 7991 iunex 7992 xpexgALT 8005 mpoexxg 8099 ixpexg 8961 ixpssmapg 8967 ttrclselem2 9764 iundom 10580 iunctb 10612 wrdexg 14559 cshwsex 17135 imasplusg 17564 imasmulr 17565 imasvsca 17567 imasip 17568 gsum2d2 20007 gsumcom2 20008 dprd2da 20077 ptcls 23640 ptcmplem2 24077 elpwiuncl 32555 aciunf1lem 32679 gsumpart 33043 gsumwrd2dccat 33053 irngval 33700 esum2dlem 34073 esum2d 34074 esumiun 34075 omssubadd 34282 eulerpartlemgs2 34362 bnj535 34883 bnj546 34889 bnj893 34921 bnj1136 34990 bnj1413 35028 weiunse 36451 numiunnum 36453 eliunov2 43669 fvmptiunrelexplb0d 43674 fvmptiunrelexplb1d 43676 iunrelexp0 43692 collexd 44253 unirnmapsn 45157 iunmapss 45158 ssmapsn 45159 iunmapsn 45160 sge0iunmptlemfi 46369 sge0iunmpt 46374 smflimlem1 46727 smfliminflem 46786 mpoexxg2 48183 |
Copyright terms: Public domain | W3C validator |