This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-nel

Description: Define negated membership. (Contributed by NM, 7-Aug-1994)

		Ref	Expression
	Assertion	df-nel	$⊢ A \notin B \leftrightarrow \neg A \in B$

Step	Hyp	Ref	Expression
0		cA	$class A$
1		cB	$class B$
2	0 1	wnel	$wff A \notin B$
3	0 1	wcel	$wff A \in B$
4	3	wn	$wff \neg A \in B$
5	2 4	wb	$wff (A \notin B \leftrightarrow \neg A \in B)$