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