Theorem opabex2

Description: Condition for an operation to be a set. (Contributed by Thierry Arnoux, 25-Jun-2019)

	Ref	Expression
Hypotheses	opabex2.1	|- ( ph -> A e. V )
	opabex2.2	|- ( ph -> B e. W )
	opabex2.3	|- ( ( ph /\ ps ) -> x e. A )
	opabex2.4	|- ( ( ph /\ ps ) -> y e. B )
Assertion	opabex2	|- ( ph -> { <. x , y >. | ps } e. _V )

Proof

Step	Hyp	Ref	Expression
1		opabex2.1	|- ( ph -> A e. V )
2		opabex2.2	|- ( ph -> B e. W )
3		opabex2.3	|- ( ( ph /\ ps ) -> x e. A )
4		opabex2.4	|- ( ( ph /\ ps ) -> y e. B )
5	1 2	xpexd	|- ( ph -> ( A X. B ) e. _V )
6	3 4	opabssxpd	|- ( ph -> { <. x , y >. | ps } C_ ( A X. B ) )
7	5 6	ssexd	|- ( ph -> { <. x , y >. | ps } e. _V )