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 V B C R A B A B C R

Proof

Step Hyp Ref Expression
1 df-res R A = R A × V
2 1 elin2 B C R A B C R B C A × V
3 opelxp B C A × V B A C V
4 elex C V C V
5 4 biantrud C V B A B A C V
6 3 5 bitr4id C V B C A × V B A
7 6 anbi1cd C V B C R B C A × V B A B C R
8 2 7 syl5bb C V B C R A B A B C R