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