Theorem elopaelxp

Description: Membership in an ordered-pair class abstraction implies membership in a Cartesian product. (Contributed by Alexander van der Vekens, 23-Jun-2018)

	Ref	Expression
Assertion	elopaelxp	|- ( A e. { <. x , y >. | ps } -> A e. ( _V X. _V ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( A = <. x , y >. /\ ps ) -> A = <. x , y >. )
2	1	2eximi	|- ( E. x E. y ( A = <. x , y >. /\ ps ) -> E. x E. y A = <. x , y >. )
3		elopab	|- ( A e. { <. x , y >. | ps } <-> E. x E. y ( A = <. x , y >. /\ ps ) )
4		elvv	|- ( A e. ( _V X. _V ) <-> E. x E. y A = <. x , y >. )
5	2 3 4	3imtr4i	|- ( A e. { <. x , y >. | ps } -> A e. ( _V X. _V ) )