![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dif32 | Structured version Visualization version GIF version |
Description: Swap second and third argument of double difference. (Contributed by NM, 18-Aug-2004.) |
Ref | Expression |
---|---|
dif32 | ⊢ ((𝐴 ∖ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∖ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uncom 4054 | . . 3 ⊢ (𝐵 ∪ 𝐶) = (𝐶 ∪ 𝐵) | |
2 | 1 | difeq2i 4021 | . 2 ⊢ (𝐴 ∖ (𝐵 ∪ 𝐶)) = (𝐴 ∖ (𝐶 ∪ 𝐵)) |
3 | difun1 4190 | . 2 ⊢ (𝐴 ∖ (𝐵 ∪ 𝐶)) = ((𝐴 ∖ 𝐵) ∖ 𝐶) | |
4 | difun1 4190 | . 2 ⊢ (𝐴 ∖ (𝐶 ∪ 𝐵)) = ((𝐴 ∖ 𝐶) ∖ 𝐵) | |
5 | 2, 3, 4 | 3eqtr3i 2790 | 1 ⊢ ((𝐴 ∖ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∖ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1539 ∖ cdif 3851 ∪ cun 3852 |
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 1912 ax-6 1971 ax-7 2016 ax-8 2114 ax-9 2122 ax-ext 2730 |
This theorem depends on definitions: df-bi 210 df-an 401 df-or 846 df-tru 1542 df-ex 1783 df-sb 2071 df-clab 2737 df-cleq 2751 df-clel 2831 df-rab 3077 df-v 3409 df-dif 3857 df-un 3859 df-in 3861 |
This theorem is referenced by: difdifdir 4378 difsnen 8612 nbupgruvtxres 27281 poimirlem25 35347 |
Copyright terms: Public domain | W3C validator |