Metamath Proof Explorer

Theorem fvsn

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

Ref Expression
Hypotheses fvsn.1 A V
fvsn.2 B V
Assertion fvsn A B A = B


Step Hyp Ref Expression
1 fvsn.1 A V
2 fvsn.2 B V
3 fvsng A V B V A B A = B
4 1 2 3 mp2an A B A = B