Theorem fnsng

Description: Functionality and domain of the singleton of an ordered pair. (Contributed by Mario Carneiro, 30-Apr-2015)

	Ref	Expression
Assertion	fnsng	$$⊢\left(A\in V\wedge B\in W\right)\to \left\{⟨A,B⟩\right\}Fn\left\{A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		funsng	$$⊢\left(A\in V\wedge B\in W\right)\to \mathrm{Fun}\left\{⟨A,B⟩\right\}$$
2		dmsnopg	$$⊢B\in W\to \mathrm{dom}\left\{⟨A,B⟩\right\}=\left\{A\right\}$$
3	2	adantl	$$⊢\left(A\in V\wedge B\in W\right)\to \mathrm{dom}\left\{⟨A,B⟩\right\}=\left\{A\right\}$$
4		df-fn	$$⊢\left\{⟨A,B⟩\right\}Fn\left\{A\right\}\leftrightarrow \left(\mathrm{Fun}\left\{⟨A,B⟩\right\}\wedge \mathrm{dom}\left\{⟨A,B⟩\right\}=\left\{A\right\}\right)$$
5	1 3 4	sylanbrc	$$⊢\left(A\in V\wedge B\in W\right)\to \left\{⟨A,B⟩\right\}Fn\left\{A\right\}$$