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	$$⊢\left(A\in V\wedge B\in W\right)\to \left\{⟨A,B⟩\right\}\left(A\right)=B$$

Proof

Step	Hyp	Ref	Expression
1		funsng	$$⊢\left(A\in V\wedge B\in W\right)\to \mathrm{Fun}\left\{⟨A,B⟩\right\}$$
2		opex	$$⊢⟨A,B⟩\in \mathrm{V}$$
3	2	snid	$$⊢⟨A,B⟩\in \left\{⟨A,B⟩\right\}$$
4		funopfv	$$⊢\mathrm{Fun}\left\{⟨A,B⟩\right\}\to \left(⟨A,B⟩\in \left\{⟨A,B⟩\right\}\to \left\{⟨A,B⟩\right\}\left(A\right)=B\right)$$
5	1 3 4	mpisyl	$$⊢\left(A\in V\wedge B\in W\right)\to \left\{⟨A,B⟩\right\}\left(A\right)=B$$