Theorem fnsng

Description: Functionality and domain of the singleton of an ordered pair. (Contributed by Mario Carneiro, 30-Apr-2015)

	Ref	Expression
Assertion	fnsng	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → { ⟨ 𝐴 , 𝐵 ⟩ } Fn { 𝐴 } )

Proof

Step	Hyp	Ref	Expression
1		funsng	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → Fun { ⟨ 𝐴 , 𝐵 ⟩ } )
2		dmsnopg	⊢ ( 𝐵 ∈ 𝑊 → dom { ⟨ 𝐴 , 𝐵 ⟩ } = { 𝐴 } )
3	2	adantl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → dom { ⟨ 𝐴 , 𝐵 ⟩ } = { 𝐴 } )
4		df-fn	⊢ ( { ⟨ 𝐴 , 𝐵 ⟩ } Fn { 𝐴 } ↔ ( Fun { ⟨ 𝐴 , 𝐵 ⟩ } ∧ dom { ⟨ 𝐴 , 𝐵 ⟩ } = { 𝐴 } ) )
5	1 3 4	sylanbrc	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → { ⟨ 𝐴 , 𝐵 ⟩ } Fn { 𝐴 } )