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	syl6bi	|- ( 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 >. ) )