Theorem equncomi 4109

Description: Inference form of equncom 4108. equncomi 4109 was automatically derived from equncomiVD 45025 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 4108	. 2 ⊢ (𝐴 = (𝐵 ∪ 𝐶) ↔ 𝐴 = (𝐶 ∪ 𝐵))
3	1, 2	mpbi 230	1 ⊢ 𝐴 = (𝐶 ∪ 𝐵)

Syntax hints:   = wceq 1541   ∪ cun 3896

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 2705

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 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903

This theorem is referenced by:  disjssun  4417  difprsn1  4753  unidmrn  6234  djucomen  10080  ackbij1lem14  10134  ltxrlt  11194  ruclem6  16151  ruclem7  16152  i1f1  25638  vtxdgoddnumeven  29553  subfacp1lem1  35295  lindsenlbs  37728  poimirlem6  37739  poimirlem7  37740  poimirlem16  37749  poimirlem17  37750  pwfi2f1o  43253  cnvrcl0  43782  iunrelexp0  43859  dfrtrcl4  43895  cotrclrcl  43899  dffrege76  44096  sucidALTVD  45026  sucidALT  45027  usgrexmpl2edg  48191