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 \mathrm{V}$$
Assertion	dfmpt	$$⊢\left(x\in A⟼B\right)=\bigcup _{x\in A}\left\{⟨x,B⟩\right\}$$

Proof

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