Theorem brprop

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

	Ref	Expression
Hypotheses	brprop.a	$$⊢\phi \to A\in V$$
	brprop.b	$$⊢\phi \to B\in W$$
	brprop.c	$$⊢\phi \to C\in V$$
	brprop.d	$$⊢\phi \to D\in W$$
Assertion	brprop	$$⊢\phi \to \left(X\left\{⟨A,B⟩,⟨C,D⟩\right\}Y\leftrightarrow \left(\left(X=A\wedge Y=B\right)\vee \left(X=C\wedge Y=D\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		brprop.a	$$⊢\phi \to A\in V$$
2		brprop.b	$$⊢\phi \to B\in W$$
3		brprop.c	$$⊢\phi \to C\in V$$
4		brprop.d	$$⊢\phi \to D\in W$$
5		df-pr	$$⊢\left\{⟨A,B⟩,⟨C,D⟩\right\}=\left\{⟨A,B⟩\right\}\cup \left\{⟨C,D⟩\right\}$$
6	5	breqi	$$⊢X\left\{⟨A,B⟩,⟨C,D⟩\right\}Y\leftrightarrow X\left(\left\{⟨A,B⟩\right\}\cup \left\{⟨C,D⟩\right\}\right)Y$$
7		brun	$$⊢X\left(\left\{⟨A,B⟩\right\}\cup \left\{⟨C,D⟩\right\}\right)Y\leftrightarrow \left(X\left\{⟨A,B⟩\right\}Y\vee X\left\{⟨C,D⟩\right\}Y\right)$$
8	6 7	bitri	$$⊢X\left\{⟨A,B⟩,⟨C,D⟩\right\}Y\leftrightarrow \left(X\left\{⟨A,B⟩\right\}Y\vee X\left\{⟨C,D⟩\right\}Y\right)$$
9		brsnop	$$⊢\left(A\in V\wedge B\in W\right)\to \left(X\left\{⟨A,B⟩\right\}Y\leftrightarrow \left(X=A\wedge Y=B\right)\right)$$
10	1 2 9	syl2anc	$$⊢\phi \to \left(X\left\{⟨A,B⟩\right\}Y\leftrightarrow \left(X=A\wedge Y=B\right)\right)$$
11		brsnop	$$⊢\left(C\in V\wedge D\in W\right)\to \left(X\left\{⟨C,D⟩\right\}Y\leftrightarrow \left(X=C\wedge Y=D\right)\right)$$
12	3 4 11	syl2anc	$$⊢\phi \to \left(X\left\{⟨C,D⟩\right\}Y\leftrightarrow \left(X=C\wedge Y=D\right)\right)$$
13	10 12	orbi12d	$$⊢\phi \to \left(\left(X\left\{⟨A,B⟩\right\}Y\vee X\left\{⟨C,D⟩\right\}Y\right)\leftrightarrow \left(\left(X=A\wedge Y=B\right)\vee \left(X=C\wedge Y=D\right)\right)\right)$$
14	8 13	bitrid	$$⊢\phi \to \left(X\left\{⟨A,B⟩,⟨C,D⟩\right\}Y\leftrightarrow \left(\left(X=A\wedge Y=B\right)\vee \left(X=C\wedge Y=D\right)\right)\right)$$