Metamath Proof Explorer


Theorem opres

Description: Ordered pair membership in a restriction when the first member belongs to the restricting class. (Contributed by NM, 30-Apr-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Hypothesis opres.1
|- B e. _V
Assertion opres
|- ( A e. D -> ( <. A , B >. e. ( C |` D ) <-> <. A , B >. e. C ) )

Proof

Step Hyp Ref Expression
1 opres.1
 |-  B e. _V
2 1 opelresi
 |-  ( <. A , B >. e. ( C |` D ) <-> ( A e. D /\ <. A , B >. e. C ) )
3 2 baib
 |-  ( A e. D -> ( <. A , B >. e. ( C |` D ) <-> <. A , B >. e. C ) )