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 4927 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) | |
2 | 1 | adantl 485 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) |
3 | abrexexg 7699 | . . . 4 ⊢ (𝐴 ∈ 𝑉 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V) | |
4 | 3 | uniexd 7498 | . . 3 ⊢ (𝐴 ∈ 𝑉 → ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V) |
5 | 4 | adantr 484 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V) |
6 | 2, 5 | eqeltrd 2834 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 = wceq 1542 ∈ wcel 2114 {cab 2717 ∀wral 3054 ∃wrex 3055 Vcvv 3400 ∪ cuni 4806 ∪ ciun 4891 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2162 ax-12 2179 ax-ext 2711 ax-rep 5164 ax-sep 5177 ax-nul 5184 ax-pr 5306 ax-un 7491 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2075 df-mo 2541 df-eu 2571 df-clab 2718 df-cleq 2731 df-clel 2812 df-nfc 2882 df-ne 2936 df-ral 3059 df-rex 3060 df-reu 3061 df-rab 3063 df-v 3402 df-sbc 3686 df-csb 3801 df-dif 3856 df-un 3858 df-in 3860 df-ss 3870 df-nul 4222 df-if 4425 df-sn 4527 df-pr 4529 df-op 4533 df-uni 4807 df-iun 4893 df-br 5041 df-opab 5103 df-mpt 5121 df-id 5439 df-xp 5541 df-rel 5542 df-cnv 5543 df-co 5544 df-dm 5545 df-rn 5546 df-res 5547 df-ima 5548 df-iota 6307 df-fun 6351 df-fn 6352 df-f 6353 df-f1 6354 df-fo 6355 df-f1o 6356 df-fv 6357 |
This theorem is referenced by: abrexex2g 7702 opabex3d 7703 opabex3rd 7704 opabex3 7705 iunex 7706 xpexgALT 7719 mpoexxg 7811 ixpexg 8544 ixpssmapg 8550 iundom 10054 iunctb 10086 wrdexg 13977 cshwsex 16549 imasplusg 16905 imasmulr 16906 imasvsca 16908 imasip 16909 gsum2d2 19225 gsumcom2 19226 dprd2da 19295 ptcls 22379 ptcmplem2 22816 elpwiuncl 30462 aciunf1lem 30586 gsumpart 30904 esum2dlem 31642 esum2d 31643 esumiun 31644 omssubadd 31849 eulerpartlemgs2 31929 bnj535 32453 bnj546 32459 bnj893 32491 bnj1136 32560 bnj1413 32598 trpredtr 33386 trpredmintr 33387 trpredrec 33394 eliunov2 40873 fvmptiunrelexplb0d 40878 fvmptiunrelexplb1d 40880 iunrelexp0 40896 collexd 41457 unirnmapsn 42332 iunmapss 42333 ssmapsn 42334 iunmapsn 42335 sge0iunmptlemfi 43533 sge0iunmpt 43538 smflimlem1 43885 smfliminflem 43942 mpoexxg2 45254 |
Copyright terms: Public domain | W3C validator |