**Description:** Inference associated with df-nel . (Contributed by BJ, 7-Jul-2018)

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

Hypothesis | neli.1 | $${\u22a2}{A}\notin {B}$$ | |

Assertion | neli | $${\u22a2}\neg {A}\in {B}$$ |

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

1 | neli.1 | $${\u22a2}{A}\notin {B}$$ | |

2 | df-nel | $${\u22a2}{A}\notin {B}\leftrightarrow \neg {A}\in {B}$$ | |

3 | 1 2 | mpbi | $${\u22a2}\neg {A}\in {B}$$ |