| 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 5008 | . 2 ⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ∪ ciun 4991 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rex 3071 df-v 3482 df-ss 3968 df-iun 4993 |
| This theorem is referenced by: iuneq12dOLD 5020 disjxiun 5140 kmlem11 10201 prmreclem4 16957 imasval 17556 iundisj 25583 iundisj2 25584 voliunlem1 25585 iunmbl 25588 volsup 25591 uniioombllem4 25621 iuninc 32573 iundisjf 32602 iundisj2f 32603 suppovss 32690 iundisjfi 32798 iundisj2fi 32799 iundisjcnt 32800 indval2 32839 sigaclcu3 34123 fiunelros 34175 meascnbl 34220 bnj1113 34799 bnj155 34893 bnj570 34919 bnj893 34942 cvmliftlem10 35299 mrsubvrs 35527 msubvrs 35565 voliunnfl 37671 volsupnfl 37672 heiborlem3 37820 heibor 37828 iunrelexp0 43715 iunp1 45071 iundjiunlem 46474 iundjiun 46475 meaiuninclem 46495 meaiuninc 46496 carageniuncllem1 46536 carageniuncllem2 46537 carageniuncl 46538 caratheodorylem1 46541 caratheodorylem2 46542 |
| Copyright terms: Public domain | W3C validator |