Metamath Proof Explorer


Theorem br1steqg

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

Ref Expression
Assertion br1steqg
|- ( ( A e. V /\ B e. W ) -> ( <. A , B >. 1st C <-> C = A ) )

Proof

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