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 4129 was automatically derived from equncomVD 41082 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 4128 | . 2 ⊢ (𝐵 ∪ 𝐶) = (𝐶 ∪ 𝐵) | |
2 | 1 | eqeq2i 2834 | 1 ⊢ (𝐴 = (𝐵 ∪ 𝐶) ↔ 𝐴 = (𝐶 ∪ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 = wceq 1528 ∪ cun 3933 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-v 3497 df-un 3940 |
This theorem is referenced by: equncomi 4130 equncomiVD 41083 |
Copyright terms: Public domain | W3C validator |