This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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