Theorem f1sn2g

Description: A function that maps a singleton to a class is injective. (Contributed by Zhi Wang, 1-Oct-2024)

	Ref	Expression
Assertion	f1sn2g	$$⊢\left(A\in V\wedge F:\left\{A\right\}⟶B\right)\to F:\left\{A\right\}\underset{1-1}{⟶}B$$

Proof

Step	Hyp	Ref	Expression
1		fsn2g	$$⊢A\in V\to \left(F:\left\{A\right\}⟶B\leftrightarrow \left(F\left(A\right)\in B\wedge F=\left\{⟨A,F\left(A\right)⟩\right\}\right)\right)$$
2	1	biimpa	$$⊢\left(A\in V\wedge F:\left\{A\right\}⟶B\right)\to \left(F\left(A\right)\in B\wedge F=\left\{⟨A,F\left(A\right)⟩\right\}\right)$$
3	2	simpld	$$⊢\left(A\in V\wedge F:\left\{A\right\}⟶B\right)\to F\left(A\right)\in B$$
4		f1sng	$$⊢\left(A\in V\wedge F\left(A\right)\in B\right)\to \left\{⟨A,F\left(A\right)⟩\right\}:\left\{A\right\}\underset{1-1}{⟶}B$$
5	3 4	syldan	$$⊢\left(A\in V\wedge F:\left\{A\right\}⟶B\right)\to \left\{⟨A,F\left(A\right)⟩\right\}:\left\{A\right\}\underset{1-1}{⟶}B$$
6		f1eq1	$$⊢F=\left\{⟨A,F\left(A\right)⟩\right\}\to \left(F:\left\{A\right\}\underset{1-1}{⟶}B\leftrightarrow \left\{⟨A,F\left(A\right)⟩\right\}:\left\{A\right\}\underset{1-1}{⟶}B\right)$$
7	2 6	simpl2im	$$⊢\left(A\in V\wedge F:\left\{A\right\}⟶B\right)\to \left(F:\left\{A\right\}\underset{1-1}{⟶}B\leftrightarrow \left\{⟨A,F\left(A\right)⟩\right\}:\left\{A\right\}\underset{1-1}{⟶}B\right)$$
8	5 7	mpbird	$$⊢\left(A\in V\wedge F:\left\{A\right\}⟶B\right)\to F:\left\{A\right\}\underset{1-1}{⟶}B$$