Theorem brin3

Description: Binary relation on an intersection is a special case of binary relation on range Cartesian product. (Contributed by Peter Mazsa, 21-Aug-2021) (Avoid depending on this detail.)

	Ref	Expression
Assertion	brin3	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\left(R\cap S\right)B\leftrightarrow AR⋉S\left\{\left\{B\right\}\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		brin2	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\left(R\cap S\right)B\leftrightarrow AR⋉S⟨B,B⟩\right)$$
2		opidg	$$⊢B\in W\to ⟨B,B⟩=\left\{\left\{B\right\}\right\}$$
3	2	adantl	$$⊢\left(A\in V\wedge B\in W\right)\to ⟨B,B⟩=\left\{\left\{B\right\}\right\}$$
4	3	breq2d	$$⊢\left(A\in V\wedge B\in W\right)\to \left(AR⋉S⟨B,B⟩\leftrightarrow AR⋉S\left\{\left\{B\right\}\right\}\right)$$
5	1 4	bitrd	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\left(R\cap S\right)B\leftrightarrow AR⋉S\left\{\left\{B\right\}\right\}\right)$$