Theorem fsnd

Description: A singleton of an ordered pair is a function. (Contributed by AV, 17-Apr-2021)

	Ref	Expression
Hypotheses	fsnd.a	$$⊢\phi \to A\in V$$
	fsnd.b	$$⊢\phi \to B\in W$$
Assertion	fsnd	$$⊢\phi \to \left\{⟨A,B⟩\right\}:\left\{A\right\}⟶W$$

Proof

Step	Hyp	Ref	Expression
1		fsnd.a	$$⊢\phi \to A\in V$$
2		fsnd.b	$$⊢\phi \to B\in W$$
3	1 2	jca	$$⊢\phi \to \left(A\in V\wedge B\in W\right)$$
4		f1sng	$$⊢\left(A\in V\wedge B\in W\right)\to \left\{⟨A,B⟩\right\}:\left\{A\right\}\underset{1-1}{⟶}W$$
5		f1f	$$⊢\left\{⟨A,B⟩\right\}:\left\{A\right\}\underset{1-1}{⟶}W\to \left\{⟨A,B⟩\right\}:\left\{A\right\}⟶W$$
6	3 4 5	3syl	$$⊢\phi \to \left\{⟨A,B⟩\right\}:\left\{A\right\}⟶W$$