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 ⊢ Ⅎ 𝑥 𝐴
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 ⊢ 𝐴 = 𝐵