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

Metamath Proof Explorer

Theorem eqrelriiv

Description: Inference from extensionality principle for relations. (Contributed by NM, 17-Mar-1995)

Ref Expression
Hypotheses eqreliiv.1 ⊢ Rel ⁡ A
eqreliiv.2 ⊢ Rel ⁡ B
eqreliiv.3 ⊢ x y ∈ A ↔ x y ∈ B
Assertion eqrelriiv ⊢ A = B

Proof

Step Hyp Ref Expression
1 eqreliiv.1 ⊢ Rel ⁡ A
2 eqreliiv.2 ⊢ Rel ⁡ B
3 eqreliiv.3 ⊢ x y ∈ A ↔ x y ∈ B
4 3 eqrelriv ⊢ Rel ⁡ A ∧ Rel ⁡ B → A = B
5 1 2 4 mp2an ⊢ A = B