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 ) ) )