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	⊢ 𝐵 ∈ V
Assertion	dfmpt	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ }

Proof

Step	Hyp	Ref	Expression
1		dfmpt.1	⊢ 𝐵 ∈ V
2		dfmpt3	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × { 𝐵 } )
3		vex	⊢ 𝑥 ∈ V
4	3 1	xpsn	⊢ ( { 𝑥 } × { 𝐵 } ) = { ⟨ 𝑥 , 𝐵 ⟩ }
5	4	a1i	⊢ ( 𝑥 ∈ 𝐴 → ( { 𝑥 } × { 𝐵 } ) = { ⟨ 𝑥 , 𝐵 ⟩ } )
6	5	iuneq2i	⊢ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × { 𝐵 } ) = ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ }
7	2 6	eqtri	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ∪ 𝑥 ∈ 𝐴 { ⟨ 𝑥 , 𝐵 ⟩ }