Metamath Proof Explorer

Theorem brresi

Description: Binary relation on a restriction. (Contributed by NM, 12-Dec-2006)

Ref Expression
Hypothesis opelresi.1 
|- C e. _V
Assertion brresi 
|- ( B ( R |` A ) C <-> ( B e. A /\ B R C ) )

Proof

Step Hyp Ref Expression
1 opelresi.1 
 |-  C e. _V
2 brres 
 |-  ( C e. _V -> ( B ( R |` A ) C <-> ( B e. A /\ B R C ) ) )
3 1 2 ax-mp 
 |-  ( B ( R |` A ) C <-> ( B e. A /\ B R C ) )