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

Metamath Proof Explorer

Theorem dfclel

Description: Characterization of the elements of a class. (Contributed by BJ, 27-Jun-2019)

		Ref	Expression
	Assertion	dfclel	$⊢ A \in B \leftrightarrow \exists x (x = A \land x \in B)$

Step	Hyp	Ref	Expression
1		cleljust	$⊢ y \in z \leftrightarrow \exists u (u = y \land u \in z)$
2		cleljust	$⊢ t \in t \leftrightarrow \exists v (v = t \land v \in t)$
3	1 2	df-clel	$⊢ A \in B \leftrightarrow \exists x (x = A \land x \in B)$