![]() |
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 5020 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶) | |
2 | iuneq2i.1 | . 2 ⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶) | |
3 | 1, 2 | mprg 3057 | 1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1534 ∈ wcel 2099 ∪ ciun 5001 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-ral 3052 df-rex 3061 df-v 3464 df-ss 3964 df-iun 5003 |
This theorem is referenced by: dfiunv2 5043 iunrab 5060 iunidOLD 5069 iunin1 5080 2iunin 5084 resiun1 6009 resiun2 6010 dfimafn2 6966 dfmpt 7158 funiunfv 7263 fpar 8130 onovuni 8372 uniqs 8806 marypha2lem2 9479 alephlim 10110 cfsmolem 10313 ituniiun 10465 imasdsval2 17531 lpival 21313 pzriprnglem10 21480 pzriprnglem11 21481 cmpsublem 23394 txbasval 23601 uniioombllem2 25603 uniioombllem4 25606 volsup2 25625 itg1addlem5 25721 itg1climres 25735 indval2 33847 sigaclfu2 33954 measvuni 34047 fmla 35209 rabiun 37294 mblfinlem2 37359 voliunnfl 37365 cnambfre 37369 uniqsALTV 38027 trclrelexplem 43378 cotrclrcl 43409 dfcoll2 43926 hoicvr 46169 hoidmv1le 46215 hoidmvle 46221 hspmbllem2 46248 smflimlem3 46394 smflimlem4 46395 smflim 46398 dfaimafn2 46779 xpiun 47535 |
Copyright terms: Public domain | W3C validator |