Theorem fnsn

Description: Functionality and domain of the singleton of an ordered pair. (Contributed by Jonathan Ben-Naim, 3-Jun-2011)

	Ref	Expression
Hypotheses	fnsn.1	$$⊢A\in \mathrm{V}$$
	fnsn.2	$$⊢B\in \mathrm{V}$$
Assertion	fnsn	$$⊢\left\{⟨A,B⟩\right\}Fn\left\{A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		fnsn.1	$$⊢A\in \mathrm{V}$$
2		fnsn.2	$$⊢B\in \mathrm{V}$$
3		fnsng	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to \left\{⟨A,B⟩\right\}Fn\left\{A\right\}$$
4	1 2 3	mp2an	$$⊢\left\{⟨A,B⟩\right\}Fn\left\{A\right\}$$