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=yz→x∈A↔yz∈A
3 vex ⊢z∈V
4 3 biantru ⊢y∈B↔y∈B∧z∈V
5 vex ⊢y∈V
6 5 3 opelrn ⊢yz∈A→z∈ran⁡A
7 6 biantrud ⊢yz∈A→y∈B↔y∈B∧z∈ran⁡A
8 4 7 bitr3id ⊢yz∈A→y∈B∧z∈V↔y∈B∧z∈ran⁡A
9 2 8 syl6bi ⊢x=yz→x∈A→y∈B∧z∈V↔y∈B∧z∈ran⁡A
10 9 com12 ⊢x∈A→x=yz→y∈B∧z∈V↔y∈B∧z∈ran⁡A
11 10 pm5.32d ⊢x∈A→x=yz∧y∈B∧z∈V↔x=yz∧y∈B∧z∈ran⁡A
12 11 2exbidv ⊢x∈A→∃y∃zx=yz∧y∈B∧z∈V↔∃y∃zx=yz∧y∈B∧z∈ran⁡A
13 elxp ⊢x∈B×V↔∃y∃zx=yz∧y∈B∧z∈V
14 elxp ⊢x∈B×ran⁡A↔∃y∃zx=yz∧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