xrninxp2

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

		Ref	Expression
	Assertion	xrninxp2	$⊢ R ⋉ S \cap (A \times (B \times C)) = \{⟨u, x⟩ \| (x \in (B \times C) \land (u \in A \land u R ⋉ S x))\}$

Step	Hyp	Ref	Expression
1		inxp2	$⊢ R ⋉ S \cap (A \times (B \times C)) = \{⟨u, x⟩ \| ((u \in A \land x \in (B \times C)) \land u R ⋉ S x)\}$
2		an21	$⊢ ((u \in A \land x \in (B \times C)) \land u R ⋉ S x) \leftrightarrow (x \in (B \times C) \land (u \in A \land u R ⋉ S x))$
3	2	opabbii	$⊢ \{⟨u, x⟩ \| ((u \in A \land x \in (B \times C)) \land u R ⋉ S x)\} = \{⟨u, x⟩ \| (x \in (B \times C) \land (u \in A \land u R ⋉ S x))\}$
4	1 3	eqtri	$⊢ R ⋉ S \cap (A \times (B \times C)) = \{⟨u, x⟩ \| (x \in (B \times C) \land (u \in A \land u R ⋉ S x))\}$

Metamath Proof Explorer