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	$$⊢A\times \left\{B\right\}=\left(x\in A⟼B\right)$$

Proof

Step	Hyp	Ref	Expression
1		velsn	$$⊢y\in \left\{B\right\}\leftrightarrow y=B$$
2	1	anbi2i	$$⊢\left(x\in A\wedge y\in \left\{B\right\}\right)\leftrightarrow \left(x\in A\wedge y=B\right)$$
3	2	opabbii	$$⊢\left\{⟨x,y⟩|\left(x\in A\wedge y\in \left\{B\right\}\right)\right\}=\left\{⟨x,y⟩|\left(x\in A\wedge y=B\right)\right\}$$
4		df-xp	$$⊢A\times \left\{B\right\}=\left\{⟨x,y⟩|\left(x\in A\wedge y\in \left\{B\right\}\right)\right\}$$
5		df-mpt	$$⊢\left(x\in A⟼B\right)=\left\{⟨x,y⟩|\left(x\in A\wedge y=B\right)\right\}$$
6	3 4 5	3eqtr4i	$$⊢A\times \left\{B\right\}=\left(x\in A⟼B\right)$$