Theorem elequ1

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

	Ref	Expression
Assertion	elequ1	$$⊢x=y\to \left(x\in z\leftrightarrow y\in z\right)$$

Proof

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