Metamath Proof Explorer


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 syl5bb
 |-  ( ph -> ( X { <. A , B >. , <. C , D >. } Y <-> ( ( X = A /\ Y = B ) \/ ( X = C /\ Y = D ) ) ) )