Theorem opabresexd

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

	Ref	Expression
Hypotheses	opabresexd.x	|- ( ( ph /\ x R y ) -> x e. C )
	opabresexd.y	|- ( ( ph /\ x R y ) -> y : A --> B )
	opabresexd.a	|- ( ( ph /\ x e. C ) -> A e. U )
	opabresexd.b	|- ( ( ph /\ x e. C ) -> B e. V )
	opabresexd.c	|- ( ph -> C e. W )
Assertion	opabresexd	|- ( ph -> { <. x , y >. | ( x R y /\ ps ) } e. _V )

Proof

Step	Hyp	Ref	Expression
1		opabresexd.x	|- ( ( ph /\ x R y ) -> x e. C )
2		opabresexd.y	|- ( ( ph /\ x R y ) -> y : A --> B )
3		opabresexd.a	|- ( ( ph /\ x e. C ) -> A e. U )
4		opabresexd.b	|- ( ( ph /\ x e. C ) -> B e. V )
5		opabresexd.c	|- ( ph -> C e. W )
6		mapex	|- ( ( A e. U /\ B e. V ) -> { y | y : A --> B } e. _V )
7	3 4 6	syl2anc	|- ( ( ph /\ x e. C ) -> { y | y : A --> B } e. _V )
8	1 2 7 5	opabresex0d	|- ( ph -> { <. x , y >. | ( x R y /\ ps ) } e. _V )