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

Definition df-vdwmc 13339
 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 13336 . 2 MonoAP
2 vk . . . . . . . . 9
32cv 1652 . . . . . . . 8
4 cvdwa 13335 . . . . . . . 8 AP
53, 4cfv 5456 . . . . . . 7 AP
65crn 4881 . . . . . 6 AP
7 vf . . . . . . . . . 10
87cv 1652 . . . . . . . . 9
98ccnv 4879 . . . . . . . 8
10 vc . . . . . . . . . 10
1110cv 1652 . . . . . . . . 9
1211csn 3816 . . . . . . . 8
139, 12cima 4883 . . . . . . 7
1413cpw 3801 . . . . . 6
156, 14cin 3321 . . . . 5 AP
16 c0 3630 . . . . 5
1715, 16wne 2601 . . . 4 AP
1817, 10wex 1551 . . 3 AP
1918, 2, 7copab 4267 . 2 AP
201, 19wceq 1653 1 MonoAP AP
 Colors of variables: wff set class This definition is referenced by:  vdwmc  13348
 Copyright terms: Public domain W3C validator