This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem opelres

Description: Ordered pair elementhood in a restriction. Exercise 13 of TakeutiZaring p. 25. (Contributed by NM, 13-Nov-1995) (Revised by BJ, 18-Feb-2022) Commute the consequent. (Revised by Peter Mazsa, 24-Sep-2022)

Ref Expression
Assertion opelres 
|- ( C e. V -> ( <. B , C >. e. ( R |` A ) <-> ( B e. A /\ <. B , C >. e. R ) ) )

Proof

Step Hyp Ref Expression
1 df-res 
 |-  ( R |` A ) = ( R i^i ( A X. _V ) )
2 1 elin2 
 |-  ( <. B , C >. e. ( R |` A ) <-> ( <. B , C >. e. R /\ <. B , C >. e. ( A X. _V ) ) )
3 opelxp 
 |-  ( <. B , C >. e. ( A X. _V ) <-> ( B e. A /\ C e. _V ) )
4 elex 
 |-  ( C e. V -> C e. _V )
5 4 biantrud 
 |-  ( C e. V -> ( B e. A <-> ( B e. A /\ C e. _V ) ) )
6 3 5 bitr4id 
 |-  ( C e. V -> ( <. B , C >. e. ( A X. _V ) <-> B e. A ) )
7 6 anbi1cd 
 |-  ( C e. V -> ( ( <. B , C >. e. R /\ <. B , C >. e. ( A X. _V ) ) <-> ( B e. A /\ <. B , C >. e. R ) ) )
8 2 7 bitrid 
 |-  ( C e. V -> ( <. B , C >. e. ( R |` A ) <-> ( B e. A /\ <. B , C >. e. R ) ) )