Theorem fconstmpt

Description: Representation of a constant function using the mapping operation. (Note that x cannot appear free in B .) (Contributed by NM, 12-Oct-1999) (Revised by Mario Carneiro, 16-Nov-2013)

	Ref	Expression
Assertion	fconstmpt	⊢ ( 𝐴 × { 𝐵 } ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		velsn	⊢ ( 𝑦 ∈ { 𝐵 } ↔ 𝑦 = 𝐵 )
2	1	anbi2i	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ { 𝐵 } ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) )
3	2	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ { 𝐵 } ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) }
4		df-xp	⊢ ( 𝐴 × { 𝐵 } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ { 𝐵 } ) }
5		df-mpt	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) }
6	3 4 5	3eqtr4i	⊢ ( 𝐴 × { 𝐵 } ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )