This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mpomptx

Description: Express a two-argument function as a one-argument function, or vice-versa. In this version B ( x ) is not assumed to be constant w.r.t x . (Contributed by Mario Carneiro, 29-Dec-2014)

		Ref	Expression
	Hypothesis	mpompt.1	$⊢ z = ⟨x, y⟩ \to C = D$
	Assertion	mpomptx	$⊢ (z \in ⋃_{x \in A} (\{x\} \times B) ⟼ C) = (x \in A, y \in B ⟼ D)$

Proof

Step	Hyp	Ref	Expression
1		mpompt.1	$⊢ z = ⟨x, y⟩ \to C = D$
2		df-mpt	$⊢ (z \in ⋃_{x \in A} (\{x\} \times B) ⟼ C) = \{⟨z, w⟩ \| (z \in ⋃_{x \in A} (\{x\} \times B) \land w = C)\}$
3		df-mpo	$⊢ (x \in A, y \in B ⟼ D) = \{⟨⟨x, y⟩, w⟩ \| ((x \in A \land y \in B) \land w = D)\}$
4		eliunxp	$⊢ z \in ⋃_{x \in A} (\{x\} \times B) \leftrightarrow \exists x \exists y (z = ⟨x, y⟩ \land (x \in A \land y \in B))$
5	4	anbi1i	$⊢ (z \in ⋃_{x \in A} (\{x\} \times B) \land w = C) \leftrightarrow (\exists x \exists y (z = ⟨x, y⟩ \land (x \in A \land y \in B)) \land w = C)$
6		19.41vv	$⊢ \exists x \exists y ((z = ⟨x, y⟩ \land (x \in A \land y \in B)) \land w = C) \leftrightarrow (\exists x \exists y (z = ⟨x, y⟩ \land (x \in A \land y \in B)) \land w = C)$
7		anass	$⊢ ((z = ⟨x, y⟩ \land (x \in A \land y \in B)) \land w = C) \leftrightarrow (z = ⟨x, y⟩ \land ((x \in A \land y \in B) \land w = C))$
8	1	eqeq2d	$⊢ z = ⟨x, y⟩ \to (w = C \leftrightarrow w = D)$
9	8	anbi2d	$⊢ z = ⟨x, y⟩ \to (((x \in A \land y \in B) \land w = C) \leftrightarrow ((x \in A \land y \in B) \land w = D))$
10	9	pm5.32i	$⊢ (z = ⟨x, y⟩ \land ((x \in A \land y \in B) \land w = C)) \leftrightarrow (z = ⟨x, y⟩ \land ((x \in A \land y \in B) \land w = D))$
11	7 10	bitri	$⊢ ((z = ⟨x, y⟩ \land (x \in A \land y \in B)) \land w = C) \leftrightarrow (z = ⟨x, y⟩ \land ((x \in A \land y \in B) \land w = D))$
12	11	2exbii	$⊢ \exists x \exists y ((z = ⟨x, y⟩ \land (x \in A \land y \in B)) \land w = C) \leftrightarrow \exists x \exists y (z = ⟨x, y⟩ \land ((x \in A \land y \in B) \land w = D))$
13	5 6 12	3bitr2i	$⊢ (z \in ⋃_{x \in A} (\{x\} \times B) \land w = C) \leftrightarrow \exists x \exists y (z = ⟨x, y⟩ \land ((x \in A \land y \in B) \land w = D))$
14	13	opabbii	$⊢ \{⟨z, w⟩ \| (z \in ⋃_{x \in A} (\{x\} \times B) \land w = C)\} = \{⟨z, w⟩ \| \exists x \exists y (z = ⟨x, y⟩ \land ((x \in A \land y \in B) \land w = D))\}$
15		dfoprab2	$⊢ \{⟨⟨x, y⟩, w⟩ \| ((x \in A \land y \in B) \land w = D)\} = \{⟨z, w⟩ \| \exists x \exists y (z = ⟨x, y⟩ \land ((x \in A \land y \in B) \land w = D))\}$
16	14 15	eqtr4i	$⊢ \{⟨z, w⟩ \| (z \in ⋃_{x \in A} (\{x\} \times B) \land w = C)\} = \{⟨⟨x, y⟩, w⟩ \| ((x \in A \land y \in B) \land w = D)\}$
17	3 16	eqtr4i	$⊢ (x \in A, y \in B ⟼ D) = \{⟨z, w⟩ \| (z \in ⋃_{x \in A} (\{x\} \times B) \land w = C)\}$
18	2 17	eqtr4i	$⊢ (z \in ⋃_{x \in A} (\{x\} \times B) ⟼ C) = (x \in A, y \in B ⟼ D)$