Theorem fvsng

Description: The value of a singleton of an ordered pair is the second member. (Contributed by NM, 26-Oct-2012) (Proof shortened by BJ, 25-Feb-2023)

	Ref	Expression
Assertion	fvsng	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( { ⟨ 𝐴 , 𝐵 ⟩ } ‘ 𝐴 ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		funsng	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → Fun { ⟨ 𝐴 , 𝐵 ⟩ } )
2		opex	⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
3	2	snid	⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝐴 , 𝐵 ⟩ }
4		funopfv	⊢ ( Fun { ⟨ 𝐴 , 𝐵 ⟩ } → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝐴 , 𝐵 ⟩ } → ( { ⟨ 𝐴 , 𝐵 ⟩ } ‘ 𝐴 ) = 𝐵 ) )
5	1 3 4	mpisyl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( { ⟨ 𝐴 , 𝐵 ⟩ } ‘ 𝐴 ) = 𝐵 )