Theorem equncom 4109

Description: If a class equals the union of two other classes, then it equals the union of those two classes commuted. equncom 4109 was automatically derived from equncomVD 45050 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

Step	Hyp	Ref	Expression
1		uncom 4108	. 2 ⊢ (𝐵 ∪ 𝐶) = (𝐶 ∪ 𝐵)
2	1	eqeq2i 2747	1 ⊢ (𝐴 = (𝐵 ∪ 𝐶) ↔ 𝐴 = (𝐶 ∪ 𝐵))

Syntax hints:   ↔ wb 206   = wceq 1541   ∪ cun 3897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-un 3904

This theorem is referenced by:  equncomi  4110  equncomiVD  45051