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

Metamath Proof Explorer

Theorem op1steq

Description: Two ways of expressing that an element is the first member of an ordered pair. (Contributed by NM, 22-Sep-2013) (Revised by Mario Carneiro, 23-Feb-2014)

Ref Expression
Assertion op1steq 
|- ( A e. ( V X. W ) -> ( ( 1st ` A ) = B <-> E. x A = <. B , x >. ) )

Proof

Step Hyp Ref Expression
1 xpss 
 |-  ( V X. W ) C_ ( _V X. _V )
2 1 sseli 
 |-  ( A e. ( V X. W ) -> A e. ( _V X. _V ) )
3 eqid 
 |-  ( 2nd ` A ) = ( 2nd ` A )
4 eqopi 
 |-  ( ( A e. ( _V X. _V ) /\ ( ( 1st ` A ) = B /\ ( 2nd ` A ) = ( 2nd ` A ) ) ) -> A = <. B , ( 2nd ` A ) >. )
5 3 4 mpanr2 
 |-  ( ( A e. ( _V X. _V ) /\ ( 1st ` A ) = B ) -> A = <. B , ( 2nd ` A ) >. )
6 fvex 
 |-  ( 2nd ` A ) e. _V
7 opeq2 
 |-  ( x = ( 2nd ` A ) -> <. B , x >. = <. B , ( 2nd ` A ) >. )
8 7 eqeq2d 
 |-  ( x = ( 2nd ` A ) -> ( A = <. B , x >. <-> A = <. B , ( 2nd ` A ) >. ) )
9 6 8 spcev 
 |-  ( A = <. B , ( 2nd ` A ) >. -> E. x A = <. B , x >. )
10 5 9 syl 
 |-  ( ( A e. ( _V X. _V ) /\ ( 1st ` A ) = B ) -> E. x A = <. B , x >. )
11 10 ex 
 |-  ( A e. ( _V X. _V ) -> ( ( 1st ` A ) = B -> E. x A = <. B , x >. ) )
12 eqop 
 |-  ( A e. ( _V X. _V ) -> ( A = <. B , x >. <-> ( ( 1st ` A ) = B /\ ( 2nd ` A ) = x ) ) )
13 simpl 
 |-  ( ( ( 1st ` A ) = B /\ ( 2nd ` A ) = x ) -> ( 1st ` A ) = B )
14 12 13 biimtrdi 
 |-  ( A e. ( _V X. _V ) -> ( A = <. B , x >. -> ( 1st ` A ) = B ) )
15 14 exlimdv 
 |-  ( A e. ( _V X. _V ) -> ( E. x A = <. B , x >. -> ( 1st ` A ) = B ) )
16 11 15 impbid 
 |-  ( A e. ( _V X. _V ) -> ( ( 1st ` A ) = B <-> E. x A = <. B , x >. ) )
17 2 16 syl 
 |-  ( A e. ( V X. W ) -> ( ( 1st ` A ) = B <-> E. x A = <. B , x >. ) )