Theorem equncomi 4131

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

Syntax hints:   = wceq 1537   ∪ cun 3934

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3941

This theorem is referenced by:  disjssun  4417  difprsn1  4733  unidmrn  6130  phplem1  8696  djucomen  9603  ackbij1lem14  9655  ltxrlt  10711  ruclem6  15588  ruclem7  15589  i1f1  24291  vtxdgoddnumeven  27335  subfacp1lem1  32426  lindsenlbs  34902  poimirlem6  34913  poimirlem7  34914  poimirlem16  34923  poimirlem17  34924  pwfi2f1o  39716  cnvrcl0  40005  iunrelexp0  40067  dfrtrcl4  40103  cotrclrcl  40107  dffrege76  40305  sucidALTVD  41224  sucidALT  41225