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

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

Detailed syntax breakdown of Definition df-vdwmc
StepHypRef Expression
1 cvdwm 14009 . 2 MonoAP
2 vk . . . . . . . . 9
32cv 1361 . . . . . . . 8
4 cvdwa 14008 . . . . . . . 8 AP
53, 4cfv 5406 . . . . . . 7 AP
65crn 4828 . . . . . 6 AP
7 vf . . . . . . . . . 10
87cv 1361 . . . . . . . . 9
98ccnv 4826 . . . . . . . 8
10 vc . . . . . . . . . 10
1110cv 1361 . . . . . . . . 9
1211csn 3865 . . . . . . . 8
139, 12cima 4830 . . . . . . 7
1413cpw 3848 . . . . . 6
156, 14cin 3315 . . . . 5 AP
16 c0 3625 . . . . 5
1715, 16wne 2596 . . . 4 AP
1817, 10wex 1589 . . 3 AP
1918, 2, 7copab 4337 . 2 AP
201, 19wceq 1362 1 MonoAP AP
 Colors of variables: wff setvar class This definition is referenced by:  vdwmc  14021
 Copyright terms: Public domain W3C validator