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

Metamath Proof Explorer

Theorem eqrd

Description: Deduce equality of classes from equivalence of membership. (Contributed by Thierry Arnoux, 21-Mar-2017) (Proof shortened by BJ, 1-Dec-2021)

	Ref	Expression
Hypotheses	eqrd.0	$⊢ Ⅎ x φ$
	eqrd.1	$⊢ \underline{Ⅎ} x A$
	eqrd.2	$⊢ \underline{Ⅎ} x B$
	eqrd.3	$⊢ φ \to (x \in A \leftrightarrow x \in B)$
Assertion	eqrd	$⊢ φ \to A = B$

Proof

Step	Hyp	Ref	Expression
1		eqrd.0	$⊢ Ⅎ x φ$
2		eqrd.1	$⊢ \underline{Ⅎ} x A$
3		eqrd.2	$⊢ \underline{Ⅎ} x B$
4		eqrd.3	$⊢ φ \to (x \in A \leftrightarrow x \in B)$
5	1 4	alrimi	$⊢ φ \to \forall x (x \in A \leftrightarrow x \in B)$
6	2 3	cleqf	$⊢ A = B \leftrightarrow \forall x (x \in A \leftrightarrow x \in B)$
7	5 6	sylibr	$⊢ φ \to A = B$