Metamath Proof Explorer

Theorem dfres2

Description: Alternate definition of the restriction operation. (Contributed by Mario Carneiro, 5-Nov-2013)

Ref Expression
Assertion dfres2 ⊢ R ↾ A = x y | x ∈ A ∧ x R y

Proof

Step Hyp Ref Expression
1 relres ⊢ Rel ⁡ R ↾ A
2 relopabv ⊢ Rel ⁡ x y | x ∈ A ∧ x R y
3 vex ⊢ z ∈ V
4 vex ⊢ w ∈ V
5 eleq1w ⊢ x = z → x ∈ A ↔ z ∈ A
6 breq1 ⊢ x = z → x R y ↔ z R y
7 5 6 anbi12d ⊢ x = z → x ∈ A ∧ x R y ↔ z ∈ A ∧ z R y
8 breq2 ⊢ y = w → z R y ↔ z R w
9 8 anbi2d ⊢ y = w → z ∈ A ∧ z R y ↔ z ∈ A ∧ z R w
10 3 4 7 9 opelopab ⊢ z w ∈ x y | x ∈ A ∧ x R y ↔ z ∈ A ∧ z R w
11 4 brresi ⊢ z R ↾ A w ↔ z ∈ A ∧ z R w
12 df-br ⊢ z R ↾ A w ↔ z w ∈ R ↾ A
13 10 11 12 3bitr2ri ⊢ z w ∈ R ↾ A ↔ z w ∈ x y | x ∈ A ∧ x R y
14 1 2 13 eqrelriiv ⊢ R ↾ A = x y | x ∈ A ∧ x R y