Metamath Proof Explorer


Theorem xrninxp2

Description: Intersection of a range Cartesian product with a Cartesian product. (Contributed by Peter Mazsa, 8-Apr-2020)

Ref Expression
Assertion xrninxp2 ( ( 𝑅𝑆 ) ∩ ( 𝐴 × ( 𝐵 × 𝐶 ) ) ) = { ⟨ 𝑢 , 𝑥 ⟩ ∣ ( 𝑥 ∈ ( 𝐵 × 𝐶 ) ∧ ( 𝑢𝐴𝑢 ( 𝑅𝑆 ) 𝑥 ) ) }

Proof

Step Hyp Ref Expression
1 inxp2 ( ( 𝑅𝑆 ) ∩ ( 𝐴 × ( 𝐵 × 𝐶 ) ) ) = { ⟨ 𝑢 , 𝑥 ⟩ ∣ ( ( 𝑢𝐴𝑥 ∈ ( 𝐵 × 𝐶 ) ) ∧ 𝑢 ( 𝑅𝑆 ) 𝑥 ) }
2 an21 ( ( ( 𝑢𝐴𝑥 ∈ ( 𝐵 × 𝐶 ) ) ∧ 𝑢 ( 𝑅𝑆 ) 𝑥 ) ↔ ( 𝑥 ∈ ( 𝐵 × 𝐶 ) ∧ ( 𝑢𝐴𝑢 ( 𝑅𝑆 ) 𝑥 ) ) )
3 2 opabbii { ⟨ 𝑢 , 𝑥 ⟩ ∣ ( ( 𝑢𝐴𝑥 ∈ ( 𝐵 × 𝐶 ) ) ∧ 𝑢 ( 𝑅𝑆 ) 𝑥 ) } = { ⟨ 𝑢 , 𝑥 ⟩ ∣ ( 𝑥 ∈ ( 𝐵 × 𝐶 ) ∧ ( 𝑢𝐴𝑢 ( 𝑅𝑆 ) 𝑥 ) ) }
4 1 3 eqtri ( ( 𝑅𝑆 ) ∩ ( 𝐴 × ( 𝐵 × 𝐶 ) ) ) = { ⟨ 𝑢 , 𝑥 ⟩ ∣ ( 𝑥 ∈ ( 𝐵 × 𝐶 ) ∧ ( 𝑢𝐴𝑢 ( 𝑅𝑆 ) 𝑥 ) ) }