Theorem brinxp

Description: Intersection of binary relation with Cartesian product. (Contributed by NM, 9-Mar-1997)

	Ref	Expression
Assertion	brinxp	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 𝑅 𝐵 ↔ 𝐴 ( 𝑅 ∩ ( 𝐶 × 𝐷 ) ) 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		brinxp2	⊢ ( 𝐴 ( 𝑅 ∩ ( 𝐶 × 𝐷 ) ) 𝐵 ↔ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) ∧ 𝐴 𝑅 𝐵 ) )
2	1	baibr	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 𝑅 𝐵 ↔ 𝐴 ( 𝑅 ∩ ( 𝐶 × 𝐷 ) ) 𝐵 ) )