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

Metamath Proof Explorer

Theorem elequ2

Description: An identity law for the non-logical predicate. (Contributed by NM, 21-Jun-1993)

		Ref	Expression
	Assertion	elequ2	$⊢ x = y \to (z \in x \leftrightarrow z \in y)$

Step	Hyp	Ref	Expression
1		ax9	$⊢ x = y \to (z \in x \to z \in y)$
2		ax9	$⊢ y = x \to (z \in y \to z \in x)$
3	2	equcoms	$⊢ x = y \to (z \in y \to z \in x)$
4	1 3	impbid	$⊢ x = y \to (z \in x \leftrightarrow z \in y)$