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

Metamath Proof Explorer

Theorem dfmpt

Description: Alternate definition for the maps-to notation df-mpt (although it requires that B be a set). (Contributed by NM, 24-Aug-2010) (Revised by Mario Carneiro, 30-Dec-2016)

		Ref	Expression
	Hypothesis	dfmpt.1	$⊢ B \in V$
	Assertion	dfmpt	$⊢ (x \in A ⟼ B) = ⋃_{x \in A} \{⟨x, B⟩\}$

Proof

Step	Hyp	Ref	Expression
1		dfmpt.1	$⊢ B \in V$
2		dfmpt3	$⊢ (x \in A ⟼ B) = ⋃_{x \in A} (\{x\} \times \{B\})$
3		vex	$⊢ x \in V$
4	3 1	xpsn	$⊢ \{x\} \times \{B\} = \{⟨x, B⟩\}$
5	4	a1i	$⊢ x \in A \to \{x\} \times \{B\} = \{⟨x, B⟩\}$
6	5	iuneq2i	$⊢ ⋃_{x \in A} (\{x\} \times \{B\}) = ⋃_{x \in A} \{⟨x, B⟩\}$
7	2 6	eqtri	$⊢ (x \in A ⟼ B) = ⋃_{x \in A} \{⟨x, B⟩\}$