Theorem equncomi 4151

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

Syntax hints:   = wceq 1541   ∪ cun 3942

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-un 3949

This theorem is referenced by:  disjssun  4463  difprsn1  4796  unidmrn  6267  phplem1OLD  9200  djucomen  10154  ackbij1lem14  10210  ltxrlt  11266  ruclem6  16160  ruclem7  16161  i1f1  25136  vtxdgoddnumeven  28675  subfacp1lem1  34001  lindsenlbs  36287  poimirlem6  36298  poimirlem7  36299  poimirlem16  36308  poimirlem17  36309  pwfi2f1o  41609  cnvrcl0  42147  iunrelexp0  42224  dfrtrcl4  42260  cotrclrcl  42264  dffrege76  42461  sucidALTVD  43402  sucidALT  43403