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

Metamath Proof Explorer

Theorem 0el

Description: Membership of the empty set in another class. (Contributed by NM, 29-Jun-2004)

		Ref	Expression
	Assertion	0el	$⊢ \emptyset \in A \leftrightarrow \exists x \in A \forall y \neg y \in x$

Step	Hyp	Ref	Expression
1		risset	$⊢ \emptyset \in A \leftrightarrow \exists x \in A x = \emptyset$
2		eq0	$⊢ x = \emptyset \leftrightarrow \forall y \neg y \in x$
3	2	rexbii	$⊢ \exists x \in A x = \emptyset \leftrightarrow \exists x \in A \forall y \neg y \in x$
4	1 3	bitri	$⊢ \emptyset \in A \leftrightarrow \exists x \in A \forall y \neg y \in x$