Theorem br2ndeq

Description: Uniqueness condition for the binary relation 2nd . (Contributed by Scott Fenton, 11-Apr-2014) (Proof shortened by Mario Carneiro, 3-May-2015)

	Ref	Expression
Hypotheses	br1steq.1	|- A e. _V
	br1steq.2	|- B e. _V
Assertion	br2ndeq	|- ( <. A , B >. 2nd C <-> C = B )

Proof

Step	Hyp	Ref	Expression
1		br1steq.1	|- A e. _V
2		br1steq.2	|- B e. _V
3		br2ndeqg	|- ( ( A e. _V /\ B e. _V ) -> ( <. A , B >. 2nd C <-> C = B ) )
4	1 2 3	mp2an	|- ( <. A , B >. 2nd C <-> C = B )