Metamath Proof Explorer

Theorem brresi2

Description: Restriction of a binary relation. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Hypothesis brresi2.1 
|- B e. _V
Assertion brresi2 
|- ( A ( R |` C ) B -> A R B )

Proof

Step Hyp Ref Expression
1 brresi2.1 
 |-  B e. _V
2 resss 
 |-  ( R |` C ) C_ R
3 2 ssbri 
 |-  ( A ( R |` C ) B -> A R B )