![]() |
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 4807 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶) | |
2 | iuneq2i.1 | . 2 ⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶) | |
3 | 1, 2 | mprg 3097 | 1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1508 ∈ wcel 2051 ∪ ciun 4789 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-ext 2745 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-clab 2754 df-cleq 2766 df-clel 2841 df-nfc 2913 df-ral 3088 df-rex 3089 df-v 3412 df-in 3831 df-ss 3838 df-iun 4791 |
This theorem is referenced by: dfiunv2 4827 iunrab 4839 iunid 4847 iunin1 4857 2iunin 4861 resiun1 5716 resiun2 5717 dfimafn2 6557 dfmpt 6728 funiunfv 6831 fpar 7618 onovuni 7782 uniqs 8156 marypha2lem2 8694 alephlim 9286 cfsmolem 9489 ituniiun 9641 imasdsval2 16644 lpival 19752 cmpsublem 21727 txbasval 21934 uniioombllem2 23903 uniioombllem4 23906 volsup2 23925 itg1addlem5 24020 itg1climres 24034 indval2 30950 sigaclfu2 31058 measvuni 31151 fmla 32224 trpred0 32629 rabiun 34339 mblfinlem2 34404 voliunnfl 34410 cnambfre 34414 uniqsALTV 35064 trclrelexplem 39453 cotrclrcl 39484 dfcoll2 39997 hoicvr 42291 hoidmv1le 42337 hoidmvle 42343 hspmbllem2 42370 smflimlem3 42510 smflimlem4 42511 smflim 42514 dfaimafn2 42801 xpiun 43431 |
Copyright terms: Public domain | W3C validator |