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

Metamath Proof Explorer

Theorem risset

Description: Two ways to say " A belongs to B ". (Contributed by NM, 22-Nov-1994)

		Ref	Expression
	Assertion	risset	$⊢ A \in B \leftrightarrow \exists x \in B x = A$

Step	Hyp	Ref	Expression
1		exancom	$⊢ \exists x (x \in B \land x = A) \leftrightarrow \exists x (x = A \land x \in B)$
2		df-rex	$⊢ \exists x \in B x = A \leftrightarrow \exists x (x \in B \land x = A)$
3		dfclel	$⊢ A \in B \leftrightarrow \exists x (x = A \land x \in B)$
4	1 2 3	3bitr4ri	$⊢ A \in B \leftrightarrow \exists x \in B x = A$