Metamath Proof Explorer

Theorem bj-dfmpoa

Description: An equivalent definition of df-mpo . (Contributed by BJ, 30-Dec-2020)

		Ref	Expression
	Assertion	bj-dfmpoa	$⊢ (x \in A, y \in B ⟼ C) = \{⟨s, t⟩ \| \exists x \in A \exists y \in B (s = ⟨x, y⟩ \land t = C)\}$

Proof

Step	Hyp	Ref	Expression
1		df-mpo	$⊢ (x \in A, y \in B ⟼ C) = \{⟨⟨x, y⟩, t⟩ \| ((x \in A \land y \in B) \land t = C)\}$
2		dfoprab2	$⊢ \{⟨⟨x, y⟩, t⟩ \| ((x \in A \land y \in B) \land t = C)\} = \{⟨s, t⟩ \| \exists x \exists y (s = ⟨x, y⟩ \land ((x \in A \land y \in B) \land t = C))\}$
3		ancom	$⊢ ((x \in A \land y \in B) \land t = C) \leftrightarrow (t = C \land (x \in A \land y \in B))$
4	3	anbi2i	$⊢ (s = ⟨x, y⟩ \land ((x \in A \land y \in B) \land t = C)) \leftrightarrow (s = ⟨x, y⟩ \land (t = C \land (x \in A \land y \in B)))$
5		anass	$⊢ ((s = ⟨x, y⟩ \land t = C) \land (x \in A \land y \in B)) \leftrightarrow (s = ⟨x, y⟩ \land (t = C \land (x \in A \land y \in B)))$
6		an13	$⊢ ((s = ⟨x, y⟩ \land t = C) \land (x \in A \land y \in B)) \leftrightarrow (y \in B \land (x \in A \land (s = ⟨x, y⟩ \land t = C)))$
7	4 5 6	3bitr2i	$⊢ (s = ⟨x, y⟩ \land ((x \in A \land y \in B) \land t = C)) \leftrightarrow (y \in B \land (x \in A \land (s = ⟨x, y⟩ \land t = C)))$
8	7	exbii	$⊢ \exists y (s = ⟨x, y⟩ \land ((x \in A \land y \in B) \land t = C)) \leftrightarrow \exists y (y \in B \land (x \in A \land (s = ⟨x, y⟩ \land t = C)))$
9		df-rex	$⊢ \exists y \in B (x \in A \land (s = ⟨x, y⟩ \land t = C)) \leftrightarrow \exists y (y \in B \land (x \in A \land (s = ⟨x, y⟩ \land t = C)))$
10		r19.42v	$⊢ \exists y \in B (x \in A \land (s = ⟨x, y⟩ \land t = C)) \leftrightarrow (x \in A \land \exists y \in B (s = ⟨x, y⟩ \land t = C))$
11	8 9 10	3bitr2i	$⊢ \exists y (s = ⟨x, y⟩ \land ((x \in A \land y \in B) \land t = C)) \leftrightarrow (x \in A \land \exists y \in B (s = ⟨x, y⟩ \land t = C))$
12	11	exbii	$⊢ \exists x \exists y (s = ⟨x, y⟩ \land ((x \in A \land y \in B) \land t = C)) \leftrightarrow \exists x (x \in A \land \exists y \in B (s = ⟨x, y⟩ \land t = C))$
13		df-rex	$⊢ \exists x \in A \exists y \in B (s = ⟨x, y⟩ \land t = C) \leftrightarrow \exists x (x \in A \land \exists y \in B (s = ⟨x, y⟩ \land t = C))$
14	12 13	bitr4i	$⊢ \exists x \exists y (s = ⟨x, y⟩ \land ((x \in A \land y \in B) \land t = C)) \leftrightarrow \exists x \in A \exists y \in B (s = ⟨x, y⟩ \land t = C)$
15	14	opabbii	$⊢ \{⟨s, t⟩ \| \exists x \exists y (s = ⟨x, y⟩ \land ((x \in A \land y \in B) \land t = C))\} = \{⟨s, t⟩ \| \exists x \in A \exists y \in B (s = ⟨x, y⟩ \land t = C)\}$
16	1 2 15	3eqtri	$⊢ (x \in A, y \in B ⟼ C) = \{⟨s, t⟩ \| \exists x \in A \exists y \in B (s = ⟨x, y⟩ \land t = C)\}$