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 4930 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶) | |
2 | iuneq2i.1 | . 2 ⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶) | |
3 | 1, 2 | mprg 3152 | 1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1533 ∈ wcel 2110 ∪ ciun 4911 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-rex 3144 df-v 3496 df-in 3942 df-ss 3951 df-iun 4913 |
This theorem is referenced by: dfiunv2 4952 iunrab 4968 iunid 4976 iunin1 4986 2iunin 4990 resiun1 5867 resiun2 5868 dfimafn2 6723 dfmpt 6900 funiunfv 7001 fpar 7805 onovuni 7973 uniqs 8351 marypha2lem2 8894 alephlim 9487 cfsmolem 9686 ituniiun 9838 imasdsval2 16783 lpival 20012 cmpsublem 22001 txbasval 22208 uniioombllem2 24178 uniioombllem4 24181 volsup2 24200 itg1addlem5 24295 itg1climres 24309 indval2 31268 sigaclfu2 31375 measvuni 31468 fmla 32623 trpred0 33070 rabiun 34859 mblfinlem2 34924 voliunnfl 34930 cnambfre 34934 uniqsALTV 35580 trclrelexplem 40049 cotrclrcl 40080 dfcoll2 40581 hoicvr 42824 hoidmv1le 42870 hoidmvle 42876 hspmbllem2 42903 smflimlem3 43043 smflimlem4 43044 smflim 43047 dfaimafn2 43359 xpiun 44027 |
Copyright terms: Public domain | W3C validator |