![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > iuneq2dv | Structured version Visualization version GIF version |
Description: Equality deduction for indexed union. (Contributed by NM, 3-Aug-2004.) |
Ref | Expression |
---|---|
iuneq2dv.1 | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) |
Ref | Expression |
---|---|
iuneq2dv | ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iuneq2dv.1 | . . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) | |
2 | 1 | ralrimiva 3115 | . 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 = 𝐶) |
3 | iuneq2 4671 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶) | |
4 | 2, 3 | syl 17 | 1 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 382 = wceq 1631 ∈ wcel 2145 ∀wral 3061 ∪ ciun 4654 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 827 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ral 3066 df-rex 3067 df-v 3353 df-in 3730 df-ss 3737 df-iun 4656 |
This theorem is referenced by: iuneq12d 4680 iuneq2d 4681 fparlem3 7429 fparlem4 7430 oalim 7765 omlim 7766 oelim 7767 oelim2 7828 r1val3 8864 imasdsval 16382 acsfn 16526 tgidm 21004 cmpsub 21423 alexsublem 22067 bcth3 23346 ovoliunlem1 23489 voliunlem1 23537 uniiccdif 23565 uniioombllem2 23570 uniioombllem3a 23571 uniioombllem4 23573 itg2monolem1 23736 taylpfval 24338 ofpreima2 29803 esum2dlem 30491 eulerpartlemgu 30776 cvmscld 31590 msubvrs 31792 mblfinlem2 33776 ftc1anclem6 33818 heibor 33948 trclfvcom 38537 meaiininclem 41216 carageniuncllem2 41252 hoidmv1le 41324 hoidmvle 41330 ovnhoilem2 41332 ovnhoi 41333 ovnlecvr2 41340 ovncvr2 41341 hspmbl 41359 ovolval4lem1 41379 ovnovollem1 41386 ovnovollem2 41387 iunhoiioo 41406 vonioolem2 41411 smflimlem4 41498 smflimlem6 41500 |
Copyright terms: Public domain | W3C validator |