NotElement Show Code edit
# Not an element () is just an abbreviation for negation and element-of.
defthm (NotElement formula (∉ A B) () () (↔ (∉ A B) (¬ (∈ A B)))
(¬ (∈ A B)) BiconditionalReflexivity
(↔ (¬ (∈ A B)) (¬ (∈ A B)))
)
edit