Metamath Proof Explorer

Theorem bj-mpomptALT

Description: Alternate proof of mpompt . (Contributed by BJ, 30-Dec-2020) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	bj-mpomptALT.1	$⊢ z = ⟨x, y⟩ \to C = D$
	Assertion	bj-mpomptALT	$⊢ (z \in (A \times B) ⟼ C) = (x \in A, y \in B ⟼ D)$

Proof

Step	Hyp	Ref	Expression
1		bj-mpomptALT.1	$⊢ z = ⟨x, y⟩ \to C = D$
2		elxp2	$⊢ z \in (A \times B) \leftrightarrow \exists x \in A \exists y \in B z = ⟨x, y⟩$
3	2	anbi1i	$⊢ (z \in (A \times B) \land t = C) \leftrightarrow (\exists x \in A \exists y \in B z = ⟨x, y⟩ \land t = C)$
4		r19.41v	$⊢ \exists x \in A (\exists y \in B z = ⟨x, y⟩ \land t = C) \leftrightarrow (\exists x \in A \exists y \in B z = ⟨x, y⟩ \land t = C)$
5		r19.41v	$⊢ \exists y \in B (z = ⟨x, y⟩ \land t = C) \leftrightarrow (\exists y \in B z = ⟨x, y⟩ \land t = C)$
6	1	eqeq2d	$⊢ z = ⟨x, y⟩ \to (t = C \leftrightarrow t = D)$
7	6	pm5.32i	$⊢ (z = ⟨x, y⟩ \land t = C) \leftrightarrow (z = ⟨x, y⟩ \land t = D)$
8	7	rexbii	$⊢ \exists y \in B (z = ⟨x, y⟩ \land t = C) \leftrightarrow \exists y \in B (z = ⟨x, y⟩ \land t = D)$
9	5 8	bitr3i	$⊢ (\exists y \in B z = ⟨x, y⟩ \land t = C) \leftrightarrow \exists y \in B (z = ⟨x, y⟩ \land t = D)$
10	9	rexbii	$⊢ \exists x \in A (\exists y \in B z = ⟨x, y⟩ \land t = C) \leftrightarrow \exists x \in A \exists y \in B (z = ⟨x, y⟩ \land t = D)$
11	3 4 10	3bitr2i	$⊢ (z \in (A \times B) \land t = C) \leftrightarrow \exists x \in A \exists y \in B (z = ⟨x, y⟩ \land t = D)$
12	11	opabbii	$⊢ \{⟨z, t⟩ \| (z \in (A \times B) \land t = C)\} = \{⟨z, t⟩ \| \exists x \in A \exists y \in B (z = ⟨x, y⟩ \land t = D)\}$
13		df-mpt	$⊢ (z \in (A \times B) ⟼ C) = \{⟨z, t⟩ \| (z \in (A \times B) \land t = C)\}$
14		bj-dfmpoa	$⊢ (x \in A, y \in B ⟼ D) = \{⟨z, t⟩ \| \exists x \in A \exists y \in B (z = ⟨x, y⟩ \land t = D)\}$
15	12 13 14	3eqtr4i	$⊢ (z \in (A \times B) ⟼ C) = (x \in A, y \in B ⟼ D)$