Description: Negation of negated membership, analogous to nne . (Contributed by Alexander van der Vekens, 18-Jan-2018) (Proof shortened by Wolf Lammen, 25-Nov-2019)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | nnel | |- ( -. A e/ B <-> A e. B ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-nel | |- ( A e/ B <-> -. A e. B ) |
|
| 2 | 1 | bicomi | |- ( -. A e. B <-> A e/ B ) |
| 3 | 2 | con1bii | |- ( -. A e/ B <-> A e. B ) |