This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elequ2g

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

		Ref	Expression
	Assertion	elequ2g	$⊢ x = y \to \forall z (z \in x \leftrightarrow z \in y)$

Step	Hyp	Ref	Expression
1		elequ2	$⊢ x = y \to (z \in x \leftrightarrow z \in y)$
2	1	alrimiv	$⊢ x = y \to \forall z (z \in x \leftrightarrow z \in y)$