Theorem bj-elequ12

Description: An identity law for the non-logical predicate, which combines elequ1 and elequ2 . For the analogous theorems for class terms, see eleq1 , eleq2 and eleq12 . TODO: move to main part. (Contributed by BJ, 29-Sep-2019)

	Ref	Expression
Assertion	bj-elequ12	$$⊢\left(x=y\wedge z=t\right)\to \left(x\in z\leftrightarrow y\in t\right)$$

Proof

Step	Hyp	Ref	Expression
1		elequ1	$$⊢x=y\to \left(x\in z\leftrightarrow y\in z\right)$$
2		elequ2	$$⊢z=t\to \left(y\in z\leftrightarrow y\in t\right)$$
3	1 2	sylan9bb	$$⊢\left(x=y\wedge z=t\right)\to \left(x\in z\leftrightarrow y\in t\right)$$