Theorem opabssxpd

Description: An ordered-pair class abstraction is a subset of a Cartesian product. Formerly part of proof for opabex2 . (Contributed by AV, 26-Nov-2021)

	Ref	Expression
Hypotheses	opabssxpd.x	|- ( ( ph /\ ps ) -> x e. A )
	opabssxpd.y	|- ( ( ph /\ ps ) -> y e. B )
Assertion	opabssxpd	|- ( ph -> { <. x , y >. | ps } C_ ( A X. B ) )

Proof

Step	Hyp	Ref	Expression
1		opabssxpd.x	|- ( ( ph /\ ps ) -> x e. A )
2		opabssxpd.y	|- ( ( ph /\ ps ) -> y e. B )
3		df-opab	|- { <. x , y >. | ps } = { z | E. x E. y ( z = <. x , y >. /\ ps ) }
4		simprl	|- ( ( ph /\ ( z = <. x , y >. /\ ps ) ) -> z = <. x , y >. )
5	1 2	opelxpd	|- ( ( ph /\ ps ) -> <. x , y >. e. ( A X. B ) )
6	5	adantrl	|- ( ( ph /\ ( z = <. x , y >. /\ ps ) ) -> <. x , y >. e. ( A X. B ) )
7	4 6	eqeltrd	|- ( ( ph /\ ( z = <. x , y >. /\ ps ) ) -> z e. ( A X. B ) )
8	7	ex	|- ( ph -> ( ( z = <. x , y >. /\ ps ) -> z e. ( A X. B ) ) )
9	8	exlimdvv	|- ( ph -> ( E. x E. y ( z = <. x , y >. /\ ps ) -> z e. ( A X. B ) ) )
10	9	abssdv	|- ( ph -> { z | E. x E. y ( z = <. x , y >. /\ ps ) } C_ ( A X. B ) )
11	3 10	eqsstrid	|- ( ph -> { <. x , y >. | ps } C_ ( A X. B ) )