This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )