Theorem br2ndeqg

Description: Uniqueness condition for the binary relation 2nd . (Contributed by Scott Fenton, 2-Jul-2020) Revised to remove sethood hypothesis on C . (Revised by Peter Mazsa, 17-Jan-2022)

	Ref	Expression
Assertion	br2ndeqg	|- ( ( A e. V /\ B e. W ) -> ( <. A , B >. 2nd C <-> C = B ) )

Proof

Step	Hyp	Ref	Expression
1		op2ndg	|- ( ( A e. V /\ B e. W ) -> ( 2nd ` <. A , B >. ) = B )
2	1	eqeq1d	|- ( ( A e. V /\ B e. W ) -> ( ( 2nd ` <. A , B >. ) = C <-> B = C ) )
3		fo2nd	|- 2nd : _V -onto-> _V
4		fofn	|- ( 2nd : _V -onto-> _V -> 2nd Fn _V )
5	3 4	ax-mp	|- 2nd Fn _V
6		opex	|- <. A , B >. e. _V
7		fnbrfvb	|- ( ( 2nd Fn _V /\ <. A , B >. e. _V ) -> ( ( 2nd ` <. A , B >. ) = C <-> <. A , B >. 2nd C ) )
8	5 6 7	mp2an	|- ( ( 2nd ` <. A , B >. ) = C <-> <. A , B >. 2nd C )
9		eqcom	|- ( B = C <-> C = B )
10	2 8 9	3bitr3g	|- ( ( A e. V /\ B e. W ) -> ( <. A , B >. 2nd C <-> C = B ) )