**Description:** Implication of membership in a class difference. (Contributed by NM, 29-Apr-1994)

Ref | Expression | ||
---|---|---|---|

Assertion | eldifi | $${\u22a2}{A}\in \left({B}\setminus {C}\right)\to {A}\in {B}$$ |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | eldif | $${\u22a2}{A}\in \left({B}\setminus {C}\right)\leftrightarrow \left({A}\in {B}\wedge \neg {A}\in {C}\right)$$ | |

2 | 1 | simplbi | $${\u22a2}{A}\in \left({B}\setminus {C}\right)\to {A}\in {B}$$ |