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 φ A V
brprop.b φ B W
brprop.c φ C V
brprop.d φ D W
Assertion brprop φ X A B C D Y X = A Y = B X = C Y = D

Proof

Step Hyp Ref Expression
1 brprop.a φ A V
2 brprop.b φ B W
3 brprop.c φ C V
4 brprop.d φ D W
5 df-pr A B C D = A B C D
6 5 breqi X A B C D Y X A B C D Y
7 brun X A B 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 V B W X A B Y X = A Y = B
10 1 2 9 syl2anc φ X A B Y X = A Y = B
11 brsnop C V D W X C D Y X = C Y = D
12 3 4 11 syl2anc φ X C D Y X = C Y = D
13 10 12 orbi12d φ X A B Y X C D Y X = A Y = B X = C Y = D
14 8 13 syl5bb φ X A B C D Y X = A Y = B X = C Y = D