dfmpt3

Description: Alternate definition for the maps-to notation df-mpt . (Contributed by Mario Carneiro, 30-Dec-2016)

		Ref	Expression
	Assertion	dfmpt3	$⊢ (x \in A ⟼ B) = ⋃_{x \in A} (\{x\} \times \{B\})$

Step	Hyp	Ref	Expression
1		df-mpt	$⊢ (x \in A ⟼ B) = \{⟨x, y⟩ \| (x \in A \land y = B)\}$
2		velsn	$⊢ y \in \{B\} \leftrightarrow y = B$
3	2	anbi2i	$⊢ (x \in A \land y \in \{B\}) \leftrightarrow (x \in A \land y = B)$
4	3	anbi2i	$⊢ (z = ⟨x, y⟩ \land (x \in A \land y \in \{B\})) \leftrightarrow (z = ⟨x, y⟩ \land (x \in A \land y = B))$
5	4	2exbii	$⊢ \exists x \exists y (z = ⟨x, y⟩ \land (x \in A \land y \in \{B\})) \leftrightarrow \exists x \exists y (z = ⟨x, y⟩ \land (x \in A \land y = B))$
6		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\}))$
7		elopab	$⊢ z \in \{⟨x, y⟩ \| (x \in A \land y = B)\} \leftrightarrow \exists x \exists y (z = ⟨x, y⟩ \land (x \in A \land y = B))$
8	5 6 7	3bitr4i	$⊢ z \in ⋃_{x \in A} (\{x\} \times \{B\}) \leftrightarrow z \in \{⟨x, y⟩ \| (x \in A \land y = B)\}$
9	8	eqriv	$⊢ ⋃_{x \in A} (\{x\} \times \{B\}) = \{⟨x, y⟩ \| (x \in A \land y = B)\}$
10	1 9	eqtr4i	$⊢ (x \in A ⟼ B) = ⋃_{x \in A} (\{x\} \times \{B\})$

Metamath Proof Explorer