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 ∈ 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 bitrid ⊢ C ∈ V → B C ∈ R ↾ A ↔ B ∈ A ∧ B C ∈ R