Theorem
elequ1
An identity law for the non-logical predicate. (Contributed by NM, 30-Jun-1993.)
Conclusion
\( \vdash x' = y' \rightarrow (x' \in z' \leftrightarrow y' \in z') \)
Proof
l0
ax8
ax8
equcoms
_
impbid
l0
_
This is the content in the right pane.