Theorem relpropg

Description: A pair of ordered pairs is a relation. (Contributed by Eric Schmidt, 24-Oct-2026)

	Ref	Expression
Assertion	relpropg	$$⊢\left(\left(A\in V\wedge B\in W\right)\wedge \left(C\in X\wedge D\in Y\right)\right)\to \mathrm{Rel}\left\{⟨A,B⟩,⟨C,D⟩\right\}$$

Proof

Step	Hyp	Ref	Expression
1		relsnopg	$$⊢\left(A\in V\wedge B\in W\right)\to \mathrm{Rel}\left\{⟨A,B⟩\right\}$$
2		relsnopg	$$⊢\left(C\in X\wedge D\in Y\right)\to \mathrm{Rel}\left\{⟨C,D⟩\right\}$$
3	1 2	anim12i	$$⊢\left(\left(A\in V\wedge B\in W\right)\wedge \left(C\in X\wedge D\in Y\right)\right)\to \left(\mathrm{Rel}\left\{⟨A,B⟩\right\}\wedge \mathrm{Rel}\left\{⟨C,D⟩\right\}\right)$$
4		relun	$$⊢\mathrm{Rel}\left(\left\{⟨A,B⟩\right\}\cup \left\{⟨C,D⟩\right\}\right)\leftrightarrow \left(\mathrm{Rel}\left\{⟨A,B⟩\right\}\wedge \mathrm{Rel}\left\{⟨C,D⟩\right\}\right)$$
5	3 4	sylibr	$$⊢\left(\left(A\in V\wedge B\in W\right)\wedge \left(C\in X\wedge D\in Y\right)\right)\to \mathrm{Rel}\left(\left\{⟨A,B⟩\right\}\cup \left\{⟨C,D⟩\right\}\right)$$
6		df-pr	$$⊢\left\{⟨A,B⟩,⟨C,D⟩\right\}=\left\{⟨A,B⟩\right\}\cup \left\{⟨C,D⟩\right\}$$
7	6	releqi	$$⊢\mathrm{Rel}\left\{⟨A,B⟩,⟨C,D⟩\right\}\leftrightarrow \mathrm{Rel}\left(\left\{⟨A,B⟩\right\}\cup \left\{⟨C,D⟩\right\}\right)$$
8	5 7	sylibr	$$⊢\left(\left(A\in V\wedge B\in W\right)\wedge \left(C\in X\wedge D\in Y\right)\right)\to \mathrm{Rel}\left\{⟨A,B⟩,⟨C,D⟩\right\}$$