Metamath Proof Explorer


Theorem brin2

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

Ref Expression
Assertion brin2 ( ( 𝐴𝑉𝐵𝑊 ) → ( 𝐴 ( 𝑅𝑆 ) 𝐵𝐴 ( 𝑅𝑆 ) ⟨ 𝐵 , 𝐵 ⟩ ) )

Proof

Step Hyp Ref Expression
1 brin ( 𝐴 ( 𝑅𝑆 ) 𝐵 ↔ ( 𝐴 𝑅 𝐵𝐴 𝑆 𝐵 ) )
2 brxrn ( ( 𝐴𝑉𝐵𝑊𝐵𝑊 ) → ( 𝐴 ( 𝑅𝑆 ) ⟨ 𝐵 , 𝐵 ⟩ ↔ ( 𝐴 𝑅 𝐵𝐴 𝑆 𝐵 ) ) )
3 2 3anidm23 ( ( 𝐴𝑉𝐵𝑊 ) → ( 𝐴 ( 𝑅𝑆 ) ⟨ 𝐵 , 𝐵 ⟩ ↔ ( 𝐴 𝑅 𝐵𝐴 𝑆 𝐵 ) ) )
4 1 3 bitr4id ( ( 𝐴𝑉𝐵𝑊 ) → ( 𝐴 ( 𝑅𝑆 ) 𝐵𝐴 ( 𝑅𝑆 ) ⟨ 𝐵 , 𝐵 ⟩ ) )