Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > iuneq2i | Structured version Visualization version GIF version |
Description: Equality inference for indexed union. (Contributed by NM, 22-Oct-2003.) |
Ref | Expression |
---|---|
iuneq2i.1 | ⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶) |
Ref | Expression |
---|---|
iuneq2i | ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iuneq2 4929 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶) | |
2 | iuneq2i.1 | . 2 ⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶) | |
3 | 1, 2 | mprg 3149 | 1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 ∈ wcel 2105 ∪ ciun 4910 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ral 3140 df-rex 3141 df-v 3494 df-in 3940 df-ss 3949 df-iun 4912 |
This theorem is referenced by: dfiunv2 4951 iunrab 4967 iunid 4975 iunin1 4985 2iunin 4989 resiun1 5866 resiun2 5867 dfimafn2 6722 dfmpt 6898 funiunfv 6998 fpar 7800 onovuni 7968 uniqs 8346 marypha2lem2 8888 alephlim 9481 cfsmolem 9680 ituniiun 9832 imasdsval2 16777 lpival 19946 cmpsublem 21935 txbasval 22142 uniioombllem2 24111 uniioombllem4 24114 volsup2 24133 itg1addlem5 24228 itg1climres 24242 indval2 31172 sigaclfu2 31279 measvuni 31372 fmla 32525 trpred0 32972 rabiun 34746 mblfinlem2 34811 voliunnfl 34817 cnambfre 34821 uniqsALTV 35467 trclrelexplem 39934 cotrclrcl 39965 dfcoll2 40465 hoicvr 42707 hoidmv1le 42753 hoidmvle 42759 hspmbllem2 42786 smflimlem3 42926 smflimlem4 42927 smflim 42930 dfaimafn2 43242 xpiun 43910 |
Copyright terms: Public domain | W3C validator |