Metamath Proof Explorer

Theorem dmres

Description: The domain of a restriction. Exercise 14 of TakeutiZaring p. 25. (Contributed by NM, 1-Aug-1994)

Ref Expression
Assertion dmres ⊢ dom ⁡ A ↾ B = B ∩ dom ⁡ A

Proof

Step Hyp Ref Expression
1 vex ⊢ x ∈ V
2 1 eldm2 ⊢ x ∈ dom ⁡ A ↾ B ↔ ∃ y x y ∈ A ↾ B
3 19.42v ⊢ ∃ y x ∈ B ∧ x y ∈ A ↔ x ∈ B ∧ ∃ y x y ∈ A
4 vex ⊢ y ∈ V
5 4 opelresi ⊢ x y ∈ A ↾ B ↔ x ∈ B ∧ x y ∈ A
6 5 exbii ⊢ ∃ y x y ∈ A ↾ B ↔ ∃ y x ∈ B ∧ x y ∈ A
7 1 eldm2 ⊢ x ∈ dom ⁡ A ↔ ∃ y x y ∈ A
8 7 anbi2i ⊢ x ∈ B ∧ x ∈ dom ⁡ A ↔ x ∈ B ∧ ∃ y x y ∈ A
9 3 6 8 3bitr4i ⊢ ∃ y x y ∈ A ↾ B ↔ x ∈ B ∧ x ∈ dom ⁡ A
10 2 9 bitr2i ⊢ x ∈ B ∧ x ∈ dom ⁡ A ↔ x ∈ dom ⁡ A ↾ B
11 10 ineqri ⊢ B ∩ dom ⁡ A = dom ⁡ A ↾ B
12 11 eqcomi ⊢ dom ⁡ A ↾ B = B ∩ dom ⁡ A