Theorem opabbrfex0d

Description: A collection of ordered pairs, the class of all possible second components being a set, is a set. (Contributed by AV, 15-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	opabbrfex0d	|- ( ph -> { <. x , y >. | x R y } 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		pm4.24	|- ( x R y <-> ( x R y /\ x R y ) )
6	5	opabbii	|- { <. x , y >. | x R y } = { <. x , y >. | ( x R y /\ x R y ) }
7	1 2 3 4	opabresex0d	|- ( ph -> { <. x , y >. | ( x R y /\ x R y ) } e. _V )
8	6 7	eqeltrid	|- ( ph -> { <. x , y >. | x R y } e. _V )