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	$$⊢\left(\phi \wedge xRy\right)\to x\in C$$
	opabresex0d.t	$$⊢\left(\phi \wedge xRy\right)\to \theta$$
	opabresex0d.y	$$⊢\left(\phi \wedge x\in C\right)\to \left\{y|\theta \right\}\in V$$
	opabresex0d.c	$$⊢\phi \to C\in W$$
Assertion	opabbrfex0d	$$⊢\phi \to \left\{⟨x,y⟩|xRy\right\}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		opabresex0d.x	$$⊢\left(\phi \wedge xRy\right)\to x\in C$$
2		opabresex0d.t	$$⊢\left(\phi \wedge xRy\right)\to \theta$$
3		opabresex0d.y	$$⊢\left(\phi \wedge x\in C\right)\to \left\{y|\theta \right\}\in V$$
4		opabresex0d.c	$$⊢\phi \to C\in W$$
5		pm4.24	$$⊢xRy\leftrightarrow \left(xRy\wedge xRy\right)$$
6	5	opabbii	$$⊢\left\{⟨x,y⟩|xRy\right\}=\left\{⟨x,y⟩|\left(xRy\wedge xRy\right)\right\}$$
7	1 2 3 4	opabresex0d	$$⊢\phi \to \left\{⟨x,y⟩|\left(xRy\wedge xRy\right)\right\}\in \mathrm{V}$$
8	6 7	eqeltrid	$$⊢\phi \to \left\{⟨x,y⟩|xRy\right\}\in \mathrm{V}$$