![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > iuneq1d | Structured version Visualization version GIF version |
Description: Equality theorem for indexed union, deduction version. (Contributed by Drahflow, 22-Oct-2015.) |
Ref | Expression |
---|---|
iuneq1d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
Ref | Expression |
---|---|
iuneq1d | ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iuneq1d.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | iuneq1 4970 | . 2 ⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1541 ∪ ciun 4954 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-rex 3074 df-v 3447 df-in 3917 df-ss 3927 df-iun 4956 |
This theorem is referenced by: iuneq12d 4982 disjxiun 5102 kmlem11 10096 prmreclem4 16791 imasval 17393 iundisj 24912 iundisj2 24913 voliunlem1 24914 iunmbl 24917 volsup 24920 uniioombllem4 24950 iuninc 31479 iundisjf 31507 iundisj2f 31508 suppovss 31598 iundisjfi 31699 iundisj2fi 31700 iundisjcnt 31701 indval2 32613 sigaclcu3 32721 fiunelros 32773 meascnbl 32818 bnj1113 33397 bnj155 33491 bnj570 33517 bnj893 33540 cvmliftlem10 33888 mrsubvrs 34116 msubvrs 34154 voliunnfl 36122 volsupnfl 36123 heiborlem3 36272 heibor 36280 iunrelexp0 41964 iunp1 43264 iundjiunlem 44690 iundjiun 44691 meaiuninclem 44711 meaiuninc 44712 carageniuncllem1 44752 carageniuncllem2 44753 carageniuncl 44754 caratheodorylem1 44757 caratheodorylem2 44758 |
Copyright terms: Public domain | W3C validator |