Description: Intersection of binary relation with Cartesian product. (Contributed by NM, 3-Mar-2007) (Revised by Mario Carneiro, 26-Apr-2015) Group conjuncts and avoid df-3an . (Revised by Peter Mazsa, 18-Sep-2022)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | brinxp2 | ⊢ ( 𝐶 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝐷 ↔ ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) ∧ 𝐶 𝑅 𝐷 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | brin | ⊢ ( 𝐶 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝐷 ↔ ( 𝐶 𝑅 𝐷 ∧ 𝐶 ( 𝐴 × 𝐵 ) 𝐷 ) ) | |
| 2 | ancom | ⊢ ( ( 𝐶 𝑅 𝐷 ∧ 𝐶 ( 𝐴 × 𝐵 ) 𝐷 ) ↔ ( 𝐶 ( 𝐴 × 𝐵 ) 𝐷 ∧ 𝐶 𝑅 𝐷 ) ) | |
| 3 | brxp | ⊢ ( 𝐶 ( 𝐴 × 𝐵 ) 𝐷 ↔ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) ) | |
| 4 | 3 | anbi1i | ⊢ ( ( 𝐶 ( 𝐴 × 𝐵 ) 𝐷 ∧ 𝐶 𝑅 𝐷 ) ↔ ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) ∧ 𝐶 𝑅 𝐷 ) ) |
| 5 | 1 2 4 | 3bitri | ⊢ ( 𝐶 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝐷 ↔ ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) ∧ 𝐶 𝑅 𝐷 ) ) |