Theorem brxp

Description: Binary relation on a Cartesian product. (Contributed by NM, 22-Apr-2004)

	Ref	Expression
Assertion	brxp	⊢ ( 𝐴 ( 𝐶 × 𝐷 ) 𝐵 ↔ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		df-br	⊢ ( 𝐴 ( 𝐶 × 𝐷 ) 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐶 × 𝐷 ) )
2		opelxp	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐶 × 𝐷 ) ↔ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) )
3	1 2	bitri	⊢ ( 𝐴 ( 𝐶 × 𝐷 ) 𝐵 ↔ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) )