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

Theorem equncom 4155
Description: If a class equals the union of two other classes, then it equals the union of those two classes commuted. equncom 4155 was automatically derived from equncomVD 43629 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 4154 . 2 (𝐵𝐶) = (𝐶𝐵)
21eqeq2i 2746 1 (𝐴 = (𝐵𝐶) ↔ 𝐴 = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1542  cun 3947
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954
This theorem is referenced by:  equncomi  4156  equncomiVD  43630
  Copyright terms: Public domain W3C validator