Theorem fnsn

Description: Functionality and domain of the singleton of an ordered pair. (Contributed by Jonathan Ben-Naim, 3-Jun-2011)

	Ref	Expression
Hypotheses	fnsn.1	⊢ 𝐴 ∈ V
	fnsn.2	⊢ 𝐵 ∈ V
Assertion	fnsn	⊢ { ⟨ 𝐴 , 𝐵 ⟩ } Fn { 𝐴 }

Proof

Step	Hyp	Ref	Expression
1		fnsn.1	⊢ 𝐴 ∈ V
2		fnsn.2	⊢ 𝐵 ∈ V
3		fnsng	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → { ⟨ 𝐴 , 𝐵 ⟩ } Fn { 𝐴 } )
4	1 2 3	mp2an	⊢ { ⟨ 𝐴 , 𝐵 ⟩ } Fn { 𝐴 }