![]() |
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 3147 | . 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 = 𝐶) |
3 | iuneq2 4727 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶) | |
4 | 2, 3 | syl 17 | 1 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 385 = wceq 1653 ∈ wcel 2157 ∀wral 3089 ∪ ciun 4710 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-ext 2777 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-ral 3094 df-rex 3095 df-v 3387 df-in 3776 df-ss 3783 df-iun 4712 |
This theorem is referenced by: iuneq12d 4736 iuneq2d 4737 fparlem3 7516 fparlem4 7517 oalim 7852 omlim 7853 oelim 7854 oelim2 7915 r1val3 8951 imasdsval 16490 acsfn 16634 tgidm 21113 cmpsub 21532 alexsublem 22176 bcth3 23457 ovoliunlem1 23610 voliunlem1 23658 uniiccdif 23686 uniioombllem2 23691 uniioombllem3a 23692 uniioombllem4 23694 itg2monolem1 23858 taylpfval 24460 ofpreima2 29985 esum2dlem 30670 eulerpartlemgu 30955 cvmscld 31772 msubvrs 31974 mblfinlem2 33936 ftc1anclem6 33978 heibor 34107 trclfvcom 38794 meaiininclem 41442 carageniuncllem2 41478 hoidmv1le 41550 hoidmvle 41556 ovnhoilem2 41558 ovnhoi 41559 ovnlecvr2 41566 ovncvr2 41567 hspmbl 41585 ovolval4lem1 41605 ovnovollem1 41612 ovnovollem2 41613 iunhoiioo 41632 vonioolem2 41637 smflimlem4 41724 smflimlem6 41726 |
Copyright terms: Public domain | W3C validator |