Metamath Proof Explorer


Theorem brsnop

Description: Binary relation for an ordered pair singleton. (Contributed by Thierry Arnoux, 23-Sep-2023)

Ref Expression
Assertion brsnop
|- ( ( A e. V /\ B e. W ) -> ( X { <. A , B >. } Y <-> ( X = A /\ Y = B ) ) )

Proof

Step Hyp Ref Expression
1 df-br
 |-  ( X { <. A , B >. } Y <-> <. X , Y >. e. { <. A , B >. } )
2 opex
 |-  <. X , Y >. e. _V
3 2 elsn
 |-  ( <. X , Y >. e. { <. A , B >. } <-> <. X , Y >. = <. A , B >. )
4 opthg2
 |-  ( ( A e. V /\ B e. W ) -> ( <. X , Y >. = <. A , B >. <-> ( X = A /\ Y = B ) ) )
5 3 4 syl5bb
 |-  ( ( A e. V /\ B e. W ) -> ( <. X , Y >. e. { <. A , B >. } <-> ( X = A /\ Y = B ) ) )
6 1 5 syl5bb
 |-  ( ( A e. V /\ B e. W ) -> ( X { <. A , B >. } Y <-> ( X = A /\ Y = B ) ) )