Theorem elopabi

Description: A consequence of membership in an ordered-pair class abstraction, using ordered pair extractors. (Contributed by NM, 29-Aug-2006)

	Ref	Expression
Hypotheses	elopabi.1	|- ( x = ( 1st ` A ) -> ( ph <-> ps ) )
	elopabi.2	|- ( y = ( 2nd ` A ) -> ( ps <-> ch ) )
Assertion	elopabi	|- ( A e. { <. x , y >. | ph } -> ch )

Proof

Step	Hyp	Ref	Expression
1		elopabi.1	|- ( x = ( 1st ` A ) -> ( ph <-> ps ) )
2		elopabi.2	|- ( y = ( 2nd ` A ) -> ( ps <-> ch ) )
3		relopabv	|- Rel { <. x , y >. | ph }
4		1st2nd	|- ( ( Rel { <. x , y >. | ph } /\ A e. { <. x , y >. | ph } ) -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. )
5	3 4	mpan	|- ( A e. { <. x , y >. | ph } -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. )
6		id	|- ( A e. { <. x , y >. | ph } -> A e. { <. x , y >. | ph } )
7	5 6	eqeltrrd	|- ( A e. { <. x , y >. | ph } -> <. ( 1st ` A ) , ( 2nd ` A ) >. e. { <. x , y >. | ph } )
8		fvex	|- ( 1st ` A ) e. _V
9		fvex	|- ( 2nd ` A ) e. _V
10	8 9 1 2	opelopab	|- ( <. ( 1st ` A ) , ( 2nd ` A ) >. e. { <. x , y >. | ph } <-> ch )
11	7 10	sylib	|- ( A e. { <. x , y >. | ph } -> ch )