Metamath Proof Explorer

Theorem dfres3

Description: Alternate definition of restriction. (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion dfres3 ⊢ A ↾ B = A ∩ B × ran ⁡ A

Proof

Step Hyp Ref Expression
1 df-res ⊢ A ↾ B = A ∩ B × V
2 eleq1 ⊢ x = y z → x ∈ A ↔ y z ∈ A
3 vex ⊢ z ∈ V
4 3 biantru ⊢ y ∈ B ↔ y ∈ B ∧ z ∈ V
5 vex ⊢ y ∈ V
6 5 3 opelrn ⊢ y z ∈ A → z ∈ ran ⁡ A
7 6 biantrud ⊢ y z ∈ A → y ∈ B ↔ y ∈ B ∧ z ∈ ran ⁡ A
8 4 7 bitr3id ⊢ y z ∈ A → y ∈ B ∧ z ∈ V ↔ y ∈ B ∧ z ∈ ran ⁡ A
9 2 8 biimtrdi ⊢ x = y z → x ∈ A → y ∈ B ∧ z ∈ V ↔ y ∈ B ∧ z ∈ ran ⁡ A
10 9 com12 ⊢ x ∈ A → x = y z → y ∈ B ∧ z ∈ V ↔ y ∈ B ∧ z ∈ ran ⁡ A
11 10 pm5.32d ⊢ x ∈ A → x = y z ∧ y ∈ B ∧ z ∈ V ↔ x = y z ∧ y ∈ B ∧ z ∈ ran ⁡ A
12 11 2exbidv ⊢ x ∈ A → ∃ y ∃ z x = y z ∧ y ∈ B ∧ z ∈ V ↔ ∃ y ∃ z x = y z ∧ y ∈ B ∧ z ∈ ran ⁡ A
13 elxp ⊢ x ∈ B × V ↔ ∃ y ∃ z x = y z ∧ y ∈ B ∧ z ∈ V
14 elxp ⊢ x ∈ B × ran ⁡ A ↔ ∃ y ∃ z x = y z ∧ y ∈ B ∧ z ∈ ran ⁡ A
15 12 13 14 3bitr4g ⊢ x ∈ A → x ∈ B × V ↔ x ∈ B × ran ⁡ A
16 15 pm5.32i ⊢ x ∈ A ∧ x ∈ B × V ↔ x ∈ A ∧ x ∈ B × ran ⁡ A
17 elin ⊢ x ∈ A ∩ B × ran ⁡ A ↔ x ∈ A ∧ x ∈ B × ran ⁡ A
18 16 17 bitr4i ⊢ x ∈ A ∧ x ∈ B × V ↔ x ∈ A ∩ B × ran ⁡ A
19 18 ineqri ⊢ A ∩ B × V = A ∩ B × ran ⁡ A
20 1 19 eqtri ⊢ A ↾ B = A ∩ B × ran ⁡ A