Theorem opabbrfexd

Description: A collection of ordered pairs, the second component being a function, is a set. (Contributed 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	opabbrfexd	|- ( ph -> { <. x , y >. | x R y } 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		pm4.24	|- ( x R y <-> ( x R y /\ x R y ) )
7	6	opabbii	|- { <. x , y >. | x R y } = { <. x , y >. | ( x R y /\ x R y ) }
8	1 2 3 4 5	opabresexd	|- ( ph -> { <. x , y >. | ( x R y /\ x R y ) } e. _V )
9	7 8	eqeltrid	|- ( ph -> { <. x , y >. | x R y } e. _V )