Theorem equncomi

Description: Inference form of equncom . equncomi was automatically derived from equncomiVD using the tools program translate__without__overwriting.cmd and minimizing. (Contributed by Alan Sare, 18-Feb-2012)

	Ref	Expression
Hypothesis	equncomi.1	$$⊢A=B\cup C$$
Assertion	equncomi	$$⊢A=C\cup B$$

Proof

Step	Hyp	Ref	Expression
1		equncomi.1	$$⊢A=B\cup C$$
2		equncom	$$⊢A=B\cup C\leftrightarrow A=C\cup B$$
3	1 2	mpbi	$$⊢A=C\cup B$$