Theorem opelinxp

Description: Ordered pair element in an intersection with Cartesian product. (Contributed by Peter Mazsa, 21-Jul-2019)

	Ref	Expression
Assertion	opelinxp	⊢ ( ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ↔ ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		brinxp2	⊢ ( 𝐶 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝐷 ↔ ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) ∧ 𝐶 𝑅 𝐷 ) )
2		df-br	⊢ ( 𝐶 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝐷 ↔ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) )
3		df-br	⊢ ( 𝐶 𝑅 𝐷 ↔ ⟨ 𝐶 , 𝐷 ⟩ ∈ 𝑅 )
4	3	anbi2i	⊢ ( ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) ∧ 𝐶 𝑅 𝐷 ) ↔ ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ 𝑅 ) )
5	1 2 4	3bitr3i	⊢ ( ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ↔ ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ 𝑅 ) )