![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > equncomi | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
equncomi.1 | ⊢ 𝐴 = (𝐵 ∪ 𝐶) |
Ref | Expression |
---|---|
equncomi | ⊢ 𝐴 = (𝐶 ∪ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | equncomi.1 | . 2 ⊢ 𝐴 = (𝐵 ∪ 𝐶) | |
2 | equncom 4150 | . 2 ⊢ (𝐴 = (𝐵 ∪ 𝐶) ↔ 𝐴 = (𝐶 ∪ 𝐵)) | |
3 | 1, 2 | mpbi 229 | 1 ⊢ 𝐴 = (𝐶 ∪ 𝐵) |
Colors of variables: wff setvar class |
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 |
Copyright terms: Public domain | W3C validator |