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 | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ( 𝑅 ∩ 𝑆 ) 𝐵 ↔ 𝐴 ( 𝑅 ⋉ 𝑆 ) 〈 𝐵 , 𝐵 〉 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | brin | ⊢ ( 𝐴 ( 𝑅 ∩ 𝑆 ) 𝐵 ↔ ( 𝐴 𝑅 𝐵 ∧ 𝐴 𝑆 𝐵 ) ) | |
2 | brxrn | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ( 𝑅 ⋉ 𝑆 ) 〈 𝐵 , 𝐵 〉 ↔ ( 𝐴 𝑅 𝐵 ∧ 𝐴 𝑆 𝐵 ) ) ) | |
3 | 2 | 3anidm23 | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ( 𝑅 ⋉ 𝑆 ) 〈 𝐵 , 𝐵 〉 ↔ ( 𝐴 𝑅 𝐵 ∧ 𝐴 𝑆 𝐵 ) ) ) |
4 | 1 3 | bitr4id | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ( 𝑅 ∩ 𝑆 ) 𝐵 ↔ 𝐴 ( 𝑅 ⋉ 𝑆 ) 〈 𝐵 , 𝐵 〉 ) ) |