Theorem brin3

Description: Binary relation on an intersection is a special case of binary relation on range Cartesian product. (Contributed by Peter Mazsa, 21-Aug-2021) (Avoid depending on this detail.)

	Ref	Expression
Assertion	brin3	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ( 𝑅 ∩ 𝑆 ) 𝐵 ↔ 𝐴 ( 𝑅 ⋉ 𝑆 ) { { 𝐵 } } ) )

Proof

Step	Hyp	Ref	Expression
1		brin2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ( 𝑅 ∩ 𝑆 ) 𝐵 ↔ 𝐴 ( 𝑅 ⋉ 𝑆 ) ⟨ 𝐵 , 𝐵 ⟩ ) )
2		opidg	⊢ ( 𝐵 ∈ 𝑊 → ⟨ 𝐵 , 𝐵 ⟩ = { { 𝐵 } } )
3	2	adantl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ⟨ 𝐵 , 𝐵 ⟩ = { { 𝐵 } } )
4	3	breq2d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ( 𝑅 ⋉ 𝑆 ) ⟨ 𝐵 , 𝐵 ⟩ ↔ 𝐴 ( 𝑅 ⋉ 𝑆 ) { { 𝐵 } } ) )
5	1 4	bitrd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ( 𝑅 ∩ 𝑆 ) 𝐵 ↔ 𝐴 ( 𝑅 ⋉ 𝑆 ) { { 𝐵 } } ) )