mpompts

Description: Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 24-Sep-2015)

		Ref	Expression
	Assertion	mpompts	$⊢ (x \in A, y \in B ⟼ C) = (z \in (A \times B) ⟼ ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ C)$

Step	Hyp	Ref	Expression
1		mpomptsx	$⊢ (x \in A, y \in B ⟼ C) = (z \in ⋃_{x \in A} (\{x\} \times B) ⟼ ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ C)$
2		iunxpconst	$⊢ ⋃_{x \in A} (\{x\} \times B) = A \times B$
3	2	mpteq1i	$⊢ (z \in ⋃_{x \in A} (\{x\} \times B) ⟼ ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ C) = (z \in (A \times B) ⟼ ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ C)$
4	1 3	eqtri	$⊢ (x \in A, y \in B ⟼ C) = (z \in (A \times B) ⟼ ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ C)$

Metamath Proof Explorer