Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  equncom Structured version   Visualization version   GIF version

Theorem equncom 4084
 Description: If a class equals the union of two other classes, then it equals the union of those two classes commuted. equncom 4084 was automatically derived from equncomVD 41745 using the tools program translate_without_overwriting.cmd and minimizing. (Contributed by Alan Sare, 18-Feb-2012.)
Assertion
Ref Expression
equncom (𝐴 = (𝐵𝐶) ↔ 𝐴 = (𝐶𝐵))

Proof of Theorem equncom
StepHypRef Expression
1 uncom 4083 . 2 (𝐵𝐶) = (𝐶𝐵)
21eqeq2i 2811 1 (𝐴 = (𝐵𝐶) ↔ 𝐴 = (𝐶𝐵))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   = wceq 1538   ∪ cun 3881 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3444  df-un 3888 This theorem is referenced by:  equncomi  4085  equncomiVD  41746
 Copyright terms: Public domain W3C validator