Theorem inxp2

Description: Intersection with a Cartesian product. (Contributed by Peter Mazsa, 18-Jul-2019)

	Ref	Expression
Assertion	inxp2	⊢ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 𝑅 𝑦 ) }

Proof

Step	Hyp	Ref	Expression
1		relinxp	⊢ Rel ( 𝑅 ∩ ( 𝐴 × 𝐵 ) )
2		dfrel4v	⊢ ( Rel ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ↔ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 } )
3	1 2	mpbi	⊢ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 }
4		brinxp2	⊢ ( 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 𝑅 𝑦 ) )
5	4	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 𝑅 𝑦 ) }
6	3 5	eqtri	⊢ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 𝑅 𝑦 ) }