Description: Lemma for chpdifbnd . (Contributed by Mario Carneiro, 25-May-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | chpdifbnd.a | |
|
chpdifbnd.1 | |
||
chpdifbnd.b | |
||
chpdifbnd.2 | |
||
chpdifbnd.c | |
||
chpdifbnd.x | |
||
chpdifbnd.y | |
||
Assertion | chpdifbndlem1 | |