Theorem opabresex0d

Description: A collection of ordered pairs, the class of all possible second components being a set, with a restriction of a binary relation is a set. (Contributed by Alexander van der Vekens, 1-Nov-2017) (Revised by AV, 1-Jan-2021)

	Ref	Expression
Hypotheses	opabresex0d.x	|- ( ( ph /\ x R y ) -> x e. C )
	opabresex0d.t	|- ( ( ph /\ x R y ) -> th )
	opabresex0d.y	|- ( ( ph /\ x e. C ) -> { y | th } e. V )
	opabresex0d.c	|- ( ph -> C e. W )
Assertion	opabresex0d	|- ( ph -> { <. x , y >. | ( x R y /\ ps ) } e. _V )

Proof

Step	Hyp	Ref	Expression
1		opabresex0d.x	|- ( ( ph /\ x R y ) -> x e. C )
2		opabresex0d.t	|- ( ( ph /\ x R y ) -> th )
3		opabresex0d.y	|- ( ( ph /\ x e. C ) -> { y | th } e. V )
4		opabresex0d.c	|- ( ph -> C e. W )
5	1 2	jca	|- ( ( ph /\ x R y ) -> ( x e. C /\ th ) )
6	5	ex	|- ( ph -> ( x R y -> ( x e. C /\ th ) ) )
7	6	alrimivv	|- ( ph -> A. x A. y ( x R y -> ( x e. C /\ th ) ) )
8	3	elexd	|- ( ( ph /\ x e. C ) -> { y | th } e. _V )
9	4 8	opabex3d	|- ( ph -> { <. x , y >. | ( x e. C /\ th ) } e. _V )
10		opabbrex	|- ( ( A. x A. y ( x R y -> ( x e. C /\ th ) ) /\ { <. x , y >. | ( x e. C /\ th ) } e. _V ) -> { <. x , y >. | ( x R y /\ ps ) } e. _V )
11	7 9 10	syl2anc	|- ( ph -> { <. x , y >. | ( x R y /\ ps ) } e. _V )