Theorem opabresex2

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) Add disjoint variable conditions betweem W , G and x , y to remove hypotheses. (Revised by SN, 13-Dec-2024)

	Ref	Expression
Assertion	opabresex2	|- { <. x , y >. | ( x ( W ` G ) y /\ th ) } e. _V

Proof

Step	Hyp	Ref	Expression
1		fvex	|- ( W ` G ) e. _V
2		elopabran	|- ( z e. { <. x , y >. | ( x ( W ` G ) y /\ th ) } -> z e. ( W ` G ) )
3	2	ssriv	|- { <. x , y >. | ( x ( W ` G ) y /\ th ) } C_ ( W ` G )
4	1 3	ssexi	|- { <. x , y >. | ( x ( W ` G ) y /\ th ) } e. _V