![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > iuneq12d | Structured version Visualization version GIF version |
Description: Equality deduction for indexed union, deduction version. (Contributed by Drahflow, 22-Oct-2015.) |
Ref | Expression |
---|---|
iuneq1d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
iuneq12d.2 | ⊢ (𝜑 → 𝐶 = 𝐷) |
Ref | Expression |
---|---|
iuneq12d | ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iuneq1d.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | 1 | iuneq1d 5025 | . 2 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶) |
3 | iuneq12d.2 | . . . 4 ⊢ (𝜑 → 𝐶 = 𝐷) | |
4 | 3 | adantr 482 | . . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 = 𝐷) |
5 | 4 | iuneq2dv 5022 | . 2 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐵 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷) |
6 | 2, 5 | eqtrd 2773 | 1 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ∈ wcel 2107 ∪ ciun 4998 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3063 df-rex 3072 df-v 3477 df-in 3956 df-ss 3966 df-iun 5000 |
This theorem is referenced by: disjiunb 5138 cfsmolem 10265 cfsmo 10266 wunex2 10733 wuncval2 10742 imasval 17457 lpival 20883 cnextval 23565 cnextfval 23566 dvfval 25414 fedgmullem1 32714 irngval 32749 mblfinlem2 36526 heiborlem10 36688 iunrelexpmin1 42459 iunrelexpmin2 42463 colleq12d 43012 |
Copyright terms: Public domain | W3C validator |