Theorem fmptsnxp

Description: Maps-to notation and Cartesian product for a singleton function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	fmptsnxp	$$⊢\left(A\in V\wedge B\in W\right)\to \left(x\in \left\{A\right\}⟼B\right)=\left\{A\right\}\times \left\{B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		xpsng	$$⊢\left(A\in V\wedge B\in W\right)\to \left\{A\right\}\times \left\{B\right\}=\left\{⟨A,B⟩\right\}$$
2		fmptsn	$$⊢\left(A\in V\wedge B\in W\right)\to \left\{⟨A,B⟩\right\}=\left(x\in \left\{A\right\}⟼B\right)$$
3	1 2	eqtr2d	$$⊢\left(A\in V\wedge B\in W\right)\to \left(x\in \left\{A\right\}⟼B\right)=\left\{A\right\}\times \left\{B\right\}$$