Theorem equncomi 4100

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

Syntax hints:   = wceq 1542   ∪ cun 3887

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894

This theorem is referenced by:  disjssun  4408  difprsn1  4745  unidmrn  6243  djucomen  10100  ackbij1lem14  10154  ltxrlt  11216  ruclem6  16202  ruclem7  16203  i1f1  25657  vtxdgoddnumeven  29622  subfacp1lem1  35361  lindsenlbs  37936  poimirlem6  37947  poimirlem7  37948  poimirlem16  37957  poimirlem17  37958  pwfi2f1o  43524  cnvrcl0  44052  iunrelexp0  44129  dfrtrcl4  44165  cotrclrcl  44169  dffrege76  44366  sucidALTVD  45296  sucidALT  45297  usgrexmpl2edg  48505