Description: If a class equals the union of two other classes, then it equals the union of those two classes commuted. equncom was automatically derived from equncomVD using the tools program translate__without__overwriting.cmd and minimizing. (Contributed by Alan Sare, 18-Feb-2012)
Ref | Expression | ||
---|---|---|---|
Assertion | equncom | |- ( A = ( B u. C ) <-> A = ( C u. B ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uncom | |- ( B u. C ) = ( C u. B ) |
|
2 | 1 | eqeq2i | |- ( A = ( B u. C ) <-> A = ( C u. B ) ) |