Theorem fnsnr

Description: If a class belongs to a function on a singleton, then that class is the obvious ordered pair. Note that this theorem also holds when A is a proper class, but its meaning is then different. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (Proof shortened by Mario Carneiro, 22-Dec-2016)

	Ref	Expression
Assertion	fnsnr	$$⊢FFn\left\{A\right\}\to \left(B\in F\to B=⟨A,F\left(A\right)⟩\right)$$

Proof

Step	Hyp	Ref	Expression
1		fnresdm	$$⊢FFn\left\{A\right\}\to {F\upharpoonright }_{\left\{A\right\}}=F$$
2		fnfun	$$⊢FFn\left\{A\right\}\to \mathrm{Fun}F$$
3		funressn	$$⊢\mathrm{Fun}F\to {F\upharpoonright }_{\left\{A\right\}}\subseteq \left\{⟨A,F\left(A\right)⟩\right\}$$
4	2 3	syl	$$⊢FFn\left\{A\right\}\to {F\upharpoonright }_{\left\{A\right\}}\subseteq \left\{⟨A,F\left(A\right)⟩\right\}$$
5	1 4	eqsstrrd	$$⊢FFn\left\{A\right\}\to F\subseteq \left\{⟨A,F\left(A\right)⟩\right\}$$
6	5	sseld	$$⊢FFn\left\{A\right\}\to \left(B\in F\to B\in \left\{⟨A,F\left(A\right)⟩\right\}\right)$$
7		elsni	$$⊢B\in \left\{⟨A,F\left(A\right)⟩\right\}\to B=⟨A,F\left(A\right)⟩$$
8	6 7	syl6	$$⊢FFn\left\{A\right\}\to \left(B\in F\to B=⟨A,F\left(A\right)⟩\right)$$