Theorem opabss

Description: The collection of ordered pairs in a class is a subclass of it. (Contributed by NM, 27-Dec-1996) (Proof shortened by Andrew Salmon, 9-Jul-2011)

	Ref	Expression
Assertion	opabss	$$⊢\left\{⟨x,y⟩|xRy\right\}\subseteq R$$

Proof

Step	Hyp	Ref	Expression
1		df-opab	$$⊢\left\{⟨x,y⟩|xRy\right\}=\left\{z|\exists x\exists y\left(z=⟨x,y⟩\wedge xRy\right)\right\}$$
2		df-br	$$⊢xRy\leftrightarrow ⟨x,y⟩\in R$$
3		eleq1	$$⊢z=⟨x,y⟩\to \left(z\in R\leftrightarrow ⟨x,y⟩\in R\right)$$
4	3	biimpar	$$⊢\left(z=⟨x,y⟩\wedge ⟨x,y⟩\in R\right)\to z\in R$$
5	2 4	sylan2b	$$⊢\left(z=⟨x,y⟩\wedge xRy\right)\to z\in R$$
6	5	exlimivv	$$⊢\exists x\exists y\left(z=⟨x,y⟩\wedge xRy\right)\to z\in R$$
7	6	abssi	$$⊢\left\{z|\exists x\exists y\left(z=⟨x,y⟩\wedge xRy\right)\right\}\subseteq R$$
8	1 7	eqsstri	$$⊢\left\{⟨x,y⟩|xRy\right\}\subseteq R$$