![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > equncom | Structured version Visualization version GIF version |
Description: If a class equals the union of two other classes, then it equals the union of those two classes commuted. equncom 4154 was automatically derived from equncomVD 43931 using the tools program translate_without_overwriting.cmd and minimizing. (Contributed by Alan Sare, 18-Feb-2012.) |
Ref | Expression |
---|---|
equncom | ⊢ (𝐴 = (𝐵 ∪ 𝐶) ↔ 𝐴 = (𝐶 ∪ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uncom 4153 | . 2 ⊢ (𝐵 ∪ 𝐶) = (𝐶 ∪ 𝐵) | |
2 | 1 | eqeq2i 2745 | 1 ⊢ (𝐴 = (𝐵 ∪ 𝐶) ↔ 𝐴 = (𝐶 ∪ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 = wceq 1541 ∪ cun 3946 |
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 2703 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-v 3476 df-un 3953 |
This theorem is referenced by: equncomi 4155 equncomiVD 43932 |
Copyright terms: Public domain | W3C validator |