Theorem rnsnf

Description: The range of a function whose domain is a singleton. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	rnsnf.1	$$⊢\phi \to A\in V$$
	rnsnf.2	$$⊢\phi \to F:\left\{A\right\}⟶B$$
Assertion	rnsnf	$$⊢\phi \to \mathrm{ran}F=\left\{F\left(A\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		rnsnf.1	$$⊢\phi \to A\in V$$
2		rnsnf.2	$$⊢\phi \to F:\left\{A\right\}⟶B$$
3		elsni	$$⊢x\in \left\{A\right\}\to x=A$$
4	3	fveq2d	$$⊢x\in \left\{A\right\}\to F\left(x\right)=F\left(A\right)$$
5	4	mpteq2ia	$$⊢\left(x\in \left\{A\right\}⟼F\left(x\right)\right)=\left(x\in \left\{A\right\}⟼F\left(A\right)\right)$$
6	2	feqmptd	$$⊢\phi \to F=\left(x\in \left\{A\right\}⟼F\left(x\right)\right)$$
7		fvexd	$$⊢\phi \to F\left(A\right)\in \mathrm{V}$$
8		fmptsn	$$⊢\left(A\in V\wedge F\left(A\right)\in \mathrm{V}\right)\to \left\{⟨A,F\left(A\right)⟩\right\}=\left(x\in \left\{A\right\}⟼F\left(A\right)\right)$$
9	1 7 8	syl2anc	$$⊢\phi \to \left\{⟨A,F\left(A\right)⟩\right\}=\left(x\in \left\{A\right\}⟼F\left(A\right)\right)$$
10	5 6 9	3eqtr4a	$$⊢\phi \to F=\left\{⟨A,F\left(A\right)⟩\right\}$$
11	10	rneqd	$$⊢\phi \to \mathrm{ran}F=\mathrm{ran}\left\{⟨A,F\left(A\right)⟩\right\}$$
12		rnsnopg	$$⊢A\in V\to \mathrm{ran}\left\{⟨A,F\left(A\right)⟩\right\}=\left\{F\left(A\right)\right\}$$
13	1 12	syl	$$⊢\phi \to \mathrm{ran}\left\{⟨A,F\left(A\right)⟩\right\}=\left\{F\left(A\right)\right\}$$
14	11 13	eqtrd	$$⊢\phi \to \mathrm{ran}F=\left\{F\left(A\right)\right\}$$