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	bitrid	|- ( ( A e. V /\ B e. W ) -> ( <. X , Y >. e. { <. A , B >. } <-> ( X = A /\ Y = B ) ) )
6	1 5	bitrid	|- ( ( A e. V /\ B e. W ) -> ( X { <. A , B >. } Y <-> ( X = A /\ Y = B ) ) )