Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
General auxiliary theorems (2)
Negated membership (alternative)
cnelbr
Next ⟩
df-nelbr
Metamath Proof Explorer
Ascii
Structured
Syntax definition
cnelbr
Description:
Extend wff notation to include the 'not elemet of' relation.
Ref
Expression
Assertion
cnelbr
class
_∉