Metamath Proof Explorer

Theorem inxprnres

Description: Restriction of a class as a class of ordered pairs. (Contributed by Peter Mazsa, 2-Jan-2019)

Ref Expression
Assertion inxprnres ⊢ R ∩ A × ran ⁡ R ↾ A = x y | x ∈ A ∧ x R y

Proof

Step Hyp Ref Expression
1 relinxp ⊢ Rel ⁡ R ∩ A × ran ⁡ R ↾ A
2 relopab ⊢ Rel ⁡ x y | x ∈ A ∧ x R y
3 eleq1w ⊢ x = z → x ∈ A ↔ z ∈ A
4 breq1 ⊢ x = z → x R y ↔ z R y
5 3 4 anbi12d ⊢ x = z → x ∈ A ∧ x R y ↔ z ∈ A ∧ z R y
6 breq2 ⊢ y = w → z R y ↔ z R w
7 6 anbi2d ⊢ y = w → z ∈ A ∧ z R y ↔ z ∈ A ∧ z R w
8 5 7 opelopabg ⊢ z ∈ V ∧ w ∈ V → z w ∈ x y | x ∈ A ∧ x R y ↔ z ∈ A ∧ z R w
9 8 el2v ⊢ z w ∈ x y | x ∈ A ∧ x R y ↔ z ∈ A ∧ z R w
10 brinxprnres ⊢ w ∈ V → z R ∩ A × ran ⁡ R ↾ A w ↔ z ∈ A ∧ z R w
11 10 elv ⊢ z R ∩ A × ran ⁡ R ↾ A w ↔ z ∈ A ∧ z R w
12 df-br ⊢ z R ∩ A × ran ⁡ R ↾ A w ↔ z w ∈ R ∩ A × ran ⁡ R ↾ A
13 9 11 12 3bitr2ri ⊢ z w ∈ R ∩ A × ran ⁡ R ↾ A ↔ z w ∈ x y | x ∈ A ∧ x R y
14 1 2 13 eqrelriiv ⊢ R ∩ A × ran ⁡ R ↾ A = x y | x ∈ A ∧ x R y