Theorem equncom 4068

Description: If a class equals the union of two other classes, then it equals the union of those two classes commuted. equncom 4068 was automatically derived from equncomVD 42161 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 4067	. 2 ⊢ (𝐵 ∪ 𝐶) = (𝐶 ∪ 𝐵)
2	1	eqeq2i 2750	1 ⊢ (𝐴 = (𝐵 ∪ 𝐶) ↔ 𝐴 = (𝐶 ∪ 𝐵))

Syntax hints:   ↔ wb 209   = wceq 1543   ∪ cun 3864

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-un 3871

This theorem is referenced by:  equncomi  4069  equncomiVD  42162