Metamath Proof Explorer

Theorem opabid2ss

Description: One direction of opabid2 which holds without a Rel A requirement. (Contributed by Thierry Arnoux, 18-Feb-2022)

Ref Expression
Assertion opabid2ss 
|- { <. x , y >. | <. x , y >. e. A } C_ A

Proof

Step Hyp Ref Expression
1 id 
 |-  ( <. x , y >. e. A -> <. x , y >. e. A )
2 1 opabssi 
 |-  { <. x , y >. | <. x , y >. e. A } C_ A