Theorem eqri

Description: Infer equality of classes from equivalence of membership. (Contributed by Thierry Arnoux, 7-Oct-2017)

	Ref	Expression
Hypotheses	eqri.1	$$⊢\underset{\_}{Ⅎ}xA$$
	eqri.2	$$⊢\underset{\_}{Ⅎ}xB$$
	eqri.3	$$⊢x\in A\leftrightarrow x\in B$$
Assertion	eqri	$$⊢A=B$$

Proof

Step	Hyp	Ref	Expression
1		eqri.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		eqri.2	$$⊢\underset{\_}{Ⅎ}xB$$
3		eqri.3	$$⊢x\in A\leftrightarrow x\in B$$
4		nftru	$$⊢Ⅎx\top$$
5	3	a1i	$$⊢\top \to \left(x\in A\leftrightarrow x\in B\right)$$
6	4 1 2 5	eqrd	$$⊢\top \to A=B$$
7	6	mptru	$$⊢A=B$$