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

Metamath Proof Explorer

Theorem opideq

Description: Equality conditions for ordered pairs <. A , A >. and <. B , B >. . (Contributed by Peter Mazsa, 22-Jul-2019) (Revised by Thierry Arnoux, 16-Feb-2022)

Ref Expression
Assertion opideq ⊢ A ∈ V → A A = B B ↔ A = B

Proof

Step Hyp Ref Expression
1 opthg ⊢ A ∈ V ∧ A ∈ V → A A = B B ↔ A = B ∧ A = B
2 1 anidms ⊢ A ∈ V → A A = B B ↔ A = B ∧ A = B
3 anidm ⊢ A = B ∧ A = B ↔ A = B
4 2 3 bitrdi ⊢ A ∈ V → A A = B B ↔ A = B