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

Metamath Proof Explorer

Theorem eqri

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

Ref Expression
Hypotheses eqri.1 ⊢ Ⅎ _ x A
eqri.2 ⊢ Ⅎ _ x B
eqri.3 ⊢ x ∈ A ↔ x ∈ B
Assertion eqri ⊢ A = B

Proof

Step Hyp Ref Expression
1 eqri.1 ⊢ Ⅎ _ x A
2 eqri.2 ⊢ Ⅎ _ x B
3 eqri.3 ⊢ x ∈ A ↔ x ∈ B
4 nftru ⊢ Ⅎ x ⊤
5 3 a1i ⊢ ⊤ → x ∈ A ↔ x ∈ B
6 4 1 2 5 eqrd ⊢ ⊤ → A = B
7 6 mptru ⊢ A = B