Theorem fsn2g

Description: A function that maps a singleton to a class is the singleton of an ordered pair. (Contributed by Thierry Arnoux, 11-Jul-2020)

	Ref	Expression
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		sneq	$$⊢a=A\to \left\{a\right\}=\left\{A\right\}$$
2	1	feq2d	$$⊢a=A\to \left(F:\left\{a\right\}⟶B\leftrightarrow F:\left\{A\right\}⟶B\right)$$
3		fveq2	$$⊢a=A\to F\left(a\right)=F\left(A\right)$$
4	3	eleq1d	$$⊢a=A\to \left(F\left(a\right)\in B\leftrightarrow F\left(A\right)\in B\right)$$
5		id	$$⊢a=A\to a=A$$
6	5 3	opeq12d	$$⊢a=A\to ⟨a,F\left(a\right)⟩=⟨A,F\left(A\right)⟩$$
7	6	sneqd	$$⊢a=A\to \left\{⟨a,F\left(a\right)⟩\right\}=\left\{⟨A,F\left(A\right)⟩\right\}$$
8	7	eqeq2d	$$⊢a=A\to \left(F=\left\{⟨a,F\left(a\right)⟩\right\}\leftrightarrow F=\left\{⟨A,F\left(A\right)⟩\right\}\right)$$
9	4 8	anbi12d	$$⊢a=A\to \left(\left(F\left(a\right)\in B\wedge F=\left\{⟨a,F\left(a\right)⟩\right\}\right)\leftrightarrow \left(F\left(A\right)\in B\wedge F=\left\{⟨A,F\left(A\right)⟩\right\}\right)\right)$$
10		vex	$$⊢a\in \mathrm{V}$$
11	10	fsn2	$$⊢F:\left\{a\right\}⟶B\leftrightarrow \left(F\left(a\right)\in B\wedge F=\left\{⟨a,F\left(a\right)⟩\right\}\right)$$
12	2 9 11	vtoclbg	$$⊢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)$$