![]() |
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 4672 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶) | |
2 | iuneq2i.1 | . 2 ⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶) | |
3 | 1, 2 | mprg 3075 | 1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1631 ∈ wcel 2145 ∪ ciun 4655 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 829 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ral 3066 df-rex 3067 df-v 3353 df-in 3731 df-ss 3738 df-iun 4657 |
This theorem is referenced by: dfiunv2 4691 iunrab 4702 iunid 4710 iunin1 4720 2iunin 4723 resiun1 5558 resiun1OLD 5559 resiun2 5560 dfimafn2 6389 dfmpt 6554 funiunfv 6650 fpar 7433 onovuni 7593 uniqs 7960 marypha2lem2 8499 alephlim 9091 cfsmolem 9295 ituniiun 9447 imasdsval2 16385 lpival 19461 cmpsublem 21424 txbasval 21631 uniioombllem2 23572 uniioombllem4 23575 volsup2 23594 itg1addlem5 23688 itg1climres 23702 indval2 30417 sigaclfu2 30525 measvuni 30618 trpred0 32073 rabiun 33716 mblfinlem2 33781 voliunnfl 33787 cnambfre 33791 uniqsALTV 34445 trclrelexplem 38530 cotrclrcl 38561 hoicvr 41283 hoidmv1le 41329 hoidmvle 41335 hspmbllem2 41362 smflimlem3 41502 smflimlem4 41503 smflim 41506 dfaimafn2 41767 xpiun 42295 |
Copyright terms: Public domain | W3C validator |