Theorem elequ12

An identity law for the non-logical predicate, which combines elequ1 and elequ2. The analogous theorems for class terms are [eleq1], [eleq2], and [eleq12] respectively. (Contributed by BJ, 29-Sep-2019.)

Conclusion
\( \vdash x' = y' \wedge z' = t' \rightarrow (x' \in z' \leftrightarrow y' \in t') \)
Proof
l0
elequ1
\( \vdash x' = y' \rightarrow (x' \in z' \leftrightarrow y' \in z') \)
elequ2
\( \vdash z' = t' \rightarrow (y' \in z' \leftrightarrow y' \in t') \)
sylan9bb l0 _