Theorem opelopab3

Description: Ordered pair membership in an ordered pair class abstraction, with a reduced hypothesis. (Contributed by Jeff Madsen, 29-May-2011)

	Ref	Expression
Hypotheses	opelopab3.1	|- ( x = A -> ( ph <-> ps ) )
	opelopab3.2	|- ( y = B -> ( ps <-> ch ) )
	opelopab3.3	|- ( ch -> A e. C )
Assertion	opelopab3	|- ( B e. D -> ( <. A , B >. e. { <. x , y >. | ph } <-> ch ) )

Proof

Step	Hyp	Ref	Expression
1		opelopab3.1	|- ( x = A -> ( ph <-> ps ) )
2		opelopab3.2	|- ( y = B -> ( ps <-> ch ) )
3		opelopab3.3	|- ( ch -> A e. C )
4		elopaelxp	|- ( <. A , B >. e. { <. x , y >. | ph } -> <. A , B >. e. ( _V X. _V ) )
5		opelxp1	|- ( <. A , B >. e. ( _V X. _V ) -> A e. _V )
6	4 5	syl	|- ( <. A , B >. e. { <. x , y >. | ph } -> A e. _V )
7	6	anim1i	|- ( ( <. A , B >. e. { <. x , y >. | ph } /\ B e. D ) -> ( A e. _V /\ B e. D ) )
8	7	ancoms	|- ( ( B e. D /\ <. A , B >. e. { <. x , y >. | ph } ) -> ( A e. _V /\ B e. D ) )
9	3	elexd	|- ( ch -> A e. _V )
10	9	anim1i	|- ( ( ch /\ B e. D ) -> ( A e. _V /\ B e. D ) )
11	10	ancoms	|- ( ( B e. D /\ ch ) -> ( A e. _V /\ B e. D ) )
12	1 2	opelopabg	|- ( ( A e. _V /\ B e. D ) -> ( <. A , B >. e. { <. x , y >. | ph } <-> ch ) )
13	8 11 12	pm5.21nd	|- ( B e. D -> ( <. A , B >. e. { <. x , y >. | ph } <-> ch ) )