Theorem brprop

Description: Binary relation for a pair of ordered pairs. (Contributed by Thierry Arnoux, 24-Sep-2023)

	Ref	Expression
Hypotheses	brprop.a	|- ( ph -> A e. V )
	brprop.b	|- ( ph -> B e. W )
	brprop.c	|- ( ph -> C e. V )
	brprop.d	|- ( ph -> D e. W )
Assertion	brprop	|- ( ph -> ( X { <. A , B >. , <. C , D >. } Y <-> ( ( X = A /\ Y = B ) \/ ( X = C /\ Y = D ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		brprop.a	|- ( ph -> A e. V )
2		brprop.b	|- ( ph -> B e. W )
3		brprop.c	|- ( ph -> C e. V )
4		brprop.d	|- ( ph -> D e. W )
5		df-pr	|- { <. A , B >. , <. C , D >. } = ( { <. A , B >. } u. { <. C , D >. } )
6	5	breqi	|- ( X { <. A , B >. , <. C , D >. } Y <-> X ( { <. A , B >. } u. { <. C , D >. } ) Y )
7		brun	|- ( X ( { <. A , B >. } u. { <. C , D >. } ) Y <-> ( X { <. A , B >. } Y \/ X { <. C , D >. } Y ) )
8	6 7	bitri	|- ( X { <. A , B >. , <. C , D >. } Y <-> ( X { <. A , B >. } Y \/ X { <. C , D >. } Y ) )
9		brsnop	|- ( ( A e. V /\ B e. W ) -> ( X { <. A , B >. } Y <-> ( X = A /\ Y = B ) ) )
10	1 2 9	syl2anc	|- ( ph -> ( X { <. A , B >. } Y <-> ( X = A /\ Y = B ) ) )
11		brsnop	|- ( ( C e. V /\ D e. W ) -> ( X { <. C , D >. } Y <-> ( X = C /\ Y = D ) ) )
12	3 4 11	syl2anc	|- ( ph -> ( X { <. C , D >. } Y <-> ( X = C /\ Y = D ) ) )
13	10 12	orbi12d	|- ( ph -> ( ( X { <. A , B >. } Y \/ X { <. C , D >. } Y ) <-> ( ( X = A /\ Y = B ) \/ ( X = C /\ Y = D ) ) ) )
14	8 13	bitrid	|- ( ph -> ( X { <. A , B >. , <. C , D >. } Y <-> ( ( X = A /\ Y = B ) \/ ( X = C /\ Y = D ) ) ) )