Theorem equncomi 4101

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

Syntax hints:   = wceq 1542   ∪ cun 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895

This theorem is referenced by:  disjssun  4409  difprsn1  4744  unidmrn  6237  djucomen  10091  ackbij1lem14  10145  ltxrlt  11207  ruclem6  16193  ruclem7  16194  i1f1  25667  vtxdgoddnumeven  29637  subfacp1lem1  35377  lindsenlbs  37950  poimirlem6  37961  poimirlem7  37962  poimirlem16  37971  poimirlem17  37972  pwfi2f1o  43542  cnvrcl0  44070  iunrelexp0  44147  dfrtrcl4  44183  cotrclrcl  44187  dffrege76  44384  sucidALTVD  45314  sucidALT  45315  usgrexmpl2edg  48517