Metamath Proof Explorer


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