Theorem equncomi 4119

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

Hypothesis

Ref	Expression
equncomi.1	⊢ 𝐴 = (𝐵 ∪ 𝐶)

Assertion

Ref	Expression
equncomi	⊢ 𝐴 = (𝐶 ∪ 𝐵)

Proof of Theorem equncomi

Step	Hyp	Ref	Expression
1		equncomi.1	. 2 ⊢ 𝐴 = (𝐵 ∪ 𝐶)
2		equncom 4118	. 2 ⊢ (𝐴 = (𝐵 ∪ 𝐶) ↔ 𝐴 = (𝐶 ∪ 𝐵))
3	1, 2	mpbi 230	1 ⊢ 𝐴 = (𝐶 ∪ 𝐵)

Syntax hints:   = wceq 1540   ∪ cun 3909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-un 3916

This theorem is referenced by:  disjssun  4427  difprsn1  4760  unidmrn  6240  djucomen  10107  ackbij1lem14  10161  ltxrlt  11220  ruclem6  16179  ruclem7  16180  i1f1  25567  vtxdgoddnumeven  29457  subfacp1lem1  35139  lindsenlbs  37582  poimirlem6  37593  poimirlem7  37594  poimirlem16  37603  poimirlem17  37604  pwfi2f1o  43058  cnvrcl0  43587  iunrelexp0  43664  dfrtrcl4  43700  cotrclrcl  43704  dffrege76  43901  sucidALTVD  44832  sucidALT  44833  usgrexmpl2edg  47993