Metamath Proof Explorer

Theorem bnj213

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Assertion bnj213 
|- _pred ( X , A , R ) C_ A

Proof

Step Hyp Ref Expression
1 df-bnj14 
 |-  _pred ( X , A , R ) = { y e. A | y R X }
2 1 ssrab3 
 |-  _pred ( X , A , R ) C_ A