Theorem br1cnvinxp

Description: Binary relation on the converse of an intersection with a Cartesian product. (Contributed by Peter Mazsa, 27-Jul-2019)

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

Proof

Step	Hyp	Ref	Expression
1		relinxp	⊢ Rel ( 𝑅 ∩ ( 𝐴 × 𝐵 ) )
2	1	relbrcnv	⊢ ( 𝐶 ◡ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝐷 ↔ 𝐷 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝐶 )
3		brinxp2	⊢ ( 𝐷 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝐶 ↔ ( ( 𝐷 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵 ) ∧ 𝐷 𝑅 𝐶 ) )
4		ancom	⊢ ( ( 𝐷 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵 ) ↔ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐴 ) )
5	4	anbi1i	⊢ ( ( ( 𝐷 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵 ) ∧ 𝐷 𝑅 𝐶 ) ↔ ( ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐴 ) ∧ 𝐷 𝑅 𝐶 ) )
6	2 3 5	3bitri	⊢ ( 𝐶 ◡ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝐷 ↔ ( ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐴 ) ∧ 𝐷 𝑅 𝐶 ) )