Theorem fsnd

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

	Ref	Expression
Hypotheses	fsnd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	fsnd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
Assertion	fsnd	⊢ ( 𝜑 → { ⟨ 𝐴 , 𝐵 ⟩ } : { 𝐴 } ⟶ 𝑊 )

Proof

Step	Hyp	Ref	Expression
1		fsnd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		fsnd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3	1 2	jca	⊢ ( 𝜑 → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) )
4		f1sng	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → { ⟨ 𝐴 , 𝐵 ⟩ } : { 𝐴 } –1-1→ 𝑊 )
5		f1f	⊢ ( { ⟨ 𝐴 , 𝐵 ⟩ } : { 𝐴 } –1-1→ 𝑊 → { ⟨ 𝐴 , 𝐵 ⟩ } : { 𝐴 } ⟶ 𝑊 )
6	3 4 5	3syl	⊢ ( 𝜑 → { ⟨ 𝐴 , 𝐵 ⟩ } : { 𝐴 } ⟶ 𝑊 )