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 4068 was automatically derived from equncomVD 42161 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 4067 | . 2 ⊢ (𝐵 ∪ 𝐶) = (𝐶 ∪ 𝐵) | |
2 | 1 | eqeq2i 2750 | 1 ⊢ (𝐴 = (𝐵 ∪ 𝐶) ↔ 𝐴 = (𝐶 ∪ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 = wceq 1543 ∪ cun 3864 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-tru 1546 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3410 df-un 3871 |
This theorem is referenced by: equncomi 4069 equncomiVD 42162 |
Copyright terms: Public domain | W3C validator |