![]() |
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 3889. equncomi 3890 was automatically derived from equncomiVD 39573 using the tools program translatewithout_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 3889 | . 2 ⊢ (𝐴 = (𝐵 ∪ 𝐶) ↔ 𝐴 = (𝐶 ∪ 𝐵)) | |
3 | 1, 2 | mpbi 220 | 1 ⊢ 𝐴 = (𝐶 ∪ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1620 ∪ cun 3701 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1859 ax-4 1874 ax-5 1976 ax-6 2042 ax-7 2078 ax-9 2136 ax-10 2156 ax-11 2171 ax-12 2184 ax-13 2379 ax-ext 2728 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1623 df-ex 1842 df-nf 1847 df-sb 2035 df-clab 2735 df-cleq 2741 df-clel 2744 df-nfc 2879 df-v 3330 df-un 3708 |
This theorem is referenced by: disjssun 4168 difprsn1 4463 unidmrn 5814 phplem1 8292 ackbij1lem14 9218 ltxrlt 10271 ruclem6 15134 ruclem7 15135 i1f1 23627 vtxdgoddnumeven 26630 subfacp1lem1 31439 lindsenlbs 33686 poimirlem6 33697 poimirlem7 33698 poimirlem16 33707 poimirlem17 33708 pwfi2f1o 38137 cnvrcl0 38403 iunrelexp0 38465 dfrtrcl4 38501 cotrclrcl 38505 dffrege76 38704 sucidALTVD 39574 sucidALT 39575 |
Copyright terms: Public domain | W3C validator |