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}\in {V}\to \left(⟨{B},{C}⟩\in \left({{R}↾}_{{A}}\right)↔\left({B}\in {A}\wedge ⟨{B},{C}⟩\in {R}\right)\right)$

Proof

Step Hyp Ref Expression
1 df-res ${⊢}{{R}↾}_{{A}}={R}\cap \left({A}×\mathrm{V}\right)$
2 1 elin2 ${⊢}⟨{B},{C}⟩\in \left({{R}↾}_{{A}}\right)↔\left(⟨{B},{C}⟩\in {R}\wedge ⟨{B},{C}⟩\in \left({A}×\mathrm{V}\right)\right)$
3 elex ${⊢}{C}\in {V}\to {C}\in \mathrm{V}$
4 3 biantrud ${⊢}{C}\in {V}\to \left({B}\in {A}↔\left({B}\in {A}\wedge {C}\in \mathrm{V}\right)\right)$
5 opelxp ${⊢}⟨{B},{C}⟩\in \left({A}×\mathrm{V}\right)↔\left({B}\in {A}\wedge {C}\in \mathrm{V}\right)$
6 4 5 syl6rbbr ${⊢}{C}\in {V}\to \left(⟨{B},{C}⟩\in \left({A}×\mathrm{V}\right)↔{B}\in {A}\right)$
7 6 anbi1cd ${⊢}{C}\in {V}\to \left(\left(⟨{B},{C}⟩\in {R}\wedge ⟨{B},{C}⟩\in \left({A}×\mathrm{V}\right)\right)↔\left({B}\in {A}\wedge ⟨{B},{C}⟩\in {R}\right)\right)$
8 2 7 syl5bb ${⊢}{C}\in {V}\to \left(⟨{B},{C}⟩\in \left({{R}↾}_{{A}}\right)↔\left({B}\in {A}\wedge ⟨{B},{C}⟩\in {R}\right)\right)$