Theorem eqri

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

	Ref	Expression
Hypotheses	eqri.1	⊢ Ⅎ 𝑥 𝐴
	eqri.2	⊢ Ⅎ 𝑥 𝐵
	eqri.3	⊢ ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 )
Assertion	eqri	⊢ 𝐴 = 𝐵

Proof

Step	Hyp	Ref	Expression
1		eqri.1	⊢ Ⅎ 𝑥 𝐴
2		eqri.2	⊢ Ⅎ 𝑥 𝐵
3		eqri.3	⊢ ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 )
4		nftru	⊢ Ⅎ 𝑥 ⊤
5	3	a1i	⊢ ( ⊤ → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )
6	4 1 2 5	eqrd	⊢ ( ⊤ → 𝐴 = 𝐵 )
7	6	mptru	⊢ 𝐴 = 𝐵