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	|- { <. x , y >. | x R y } C_ R

Proof

Step	Hyp	Ref	Expression
1		df-opab	|- { <. x , y >. | x R y } = { z | E. x E. y ( z = <. x , y >. /\ x R y ) }
2		df-br	|- ( x R y <-> <. x , y >. e. R )
3		eleq1	|- ( z = <. x , y >. -> ( z e. R <-> <. x , y >. e. R ) )
4	3	biimpar	|- ( ( z = <. x , y >. /\ <. x , y >. e. R ) -> z e. R )
5	2 4	sylan2b	|- ( ( z = <. x , y >. /\ x R y ) -> z e. R )
6	5	exlimivv	|- ( E. x E. y ( z = <. x , y >. /\ x R y ) -> z e. R )
7	6	abssi	|- { z | E. x E. y ( z = <. x , y >. /\ x R y ) } C_ R
8	1 7	eqsstri	|- { <. x , y >. | x R y } C_ R