Theorem elequ2g

A form of elequ2 with a universal quantifier. Its converse is the axiom of extensionality [ax-ext]. (Contributed by BJ, 3-Oct-2019.)

Conclusion

\( \vdash x' = y' \rightarrow \forall z \, (z \in x' \leftrightarrow z \in y') \)

Proof

elequ2

alrimiv _