Metamath Proof Explorer


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 { 𝐴 }