Theorem opabresex2d

Description: Restrictions of a collection of ordered pairs of related elements are sets. (Contributed by Alexander van der Vekens, 1-Nov-2017) (Revised by AV, 15-Jan-2021)

	Ref	Expression
Hypotheses	opabresex2d.1	|- ( ( ph /\ x ( W ` G ) y ) -> ps )
	opabresex2d.2	|- ( ph -> { <. x , y >. | ps } e. V )
Assertion	opabresex2d	|- ( ph -> { <. x , y >. | ( x ( W ` G ) y /\ th ) } e. _V )

Proof

Step	Hyp	Ref	Expression
1		opabresex2d.1	|- ( ( ph /\ x ( W ` G ) y ) -> ps )
2		opabresex2d.2	|- ( ph -> { <. x , y >. | ps } e. V )
3	1	ex	|- ( ph -> ( x ( W ` G ) y -> ps ) )
4	3	alrimivv	|- ( ph -> A. x A. y ( x ( W ` G ) y -> ps ) )
5		opabbrex	|- ( ( A. x A. y ( x ( W ` G ) y -> ps ) /\ { <. x , y >. | ps } e. V ) -> { <. x , y >. | ( x ( W ` G ) y /\ th ) } e. _V )
6	4 2 5	syl2anc	|- ( ph -> { <. x , y >. | ( x ( W ` G ) y /\ th ) } e. _V )