Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-vdwmc Unicode version

Definition df-vdwmc 14487
 Description: Define the "contains a monochromatic AP" predicate. (Contributed by Mario Carneiro, 18-Aug-2014.)
Assertion
Ref Expression
df-vdwmc
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-vdwmc
StepHypRef Expression
1 cvdwm 14484 . 2
2 vk . . . . . . . . 9
32cv 1394 . . . . . . . 8
4 cvdwa 14483 . . . . . . . 8
53, 4cfv 5593 . . . . . . 7
65crn 5005 . . . . . 6
7 vf . . . . . . . . . 10
87cv 1394 . . . . . . . . 9
98ccnv 5003 . . . . . . . 8
10 vc . . . . . . . . . 10
1110cv 1394 . . . . . . . . 9
1211csn 4029 . . . . . . . 8
139, 12cima 5007 . . . . . . 7
1413cpw 4012 . . . . . 6
156, 14cin 3474 . . . . 5
16 c0 3784 . . . . 5
1715, 16wne 2652 . . . 4
1817, 10wex 1612 . . 3
1918, 2, 7copab 4509 . 2
201, 19wceq 1395 1
 Colors of variables: wff setvar class This definition is referenced by:  vdwmc  14496
 Copyright terms: Public domain W3C validator