Theorem elequ2

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

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

Proof

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