Theorem equncomi 4090

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

Syntax hints:   = wceq 1547   ∪ cun 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888

This theorem is referenced by:  disjssun  4396  difprsn1  4733  unidmrn  6230  djucomen  10091  ackbij1lem14  10145  ltxrlt  11207  ruclem6  16193  ruclem7  16194  i1f1  25675  vtxdgoddnumeven  29640  subfacp1lem1  35407  lindsenlbs  37982  poimirlem6  37993  poimirlem7  37994  poimirlem16  38003  poimirlem17  38004  pwfi2f1o  43541  cnvrcl0  44069  iunrelexp0  44146  dfrtrcl4  44182  cotrclrcl  44186  dffrege76  44383  sucidALTVD  45313  sucidALT  45314  usgrexmpl2edg  48520