# 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 ${⊢}\mathrm{dom}\left({{A}↾}_{{B}}\right)={B}\cap \mathrm{dom}{A}$

### Proof

Step Hyp Ref Expression
1 vex ${⊢}{x}\in \mathrm{V}$
2 1 eldm2 ${⊢}{x}\in \mathrm{dom}\left({{A}↾}_{{B}}\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩\in \left({{A}↾}_{{B}}\right)$
3 19.42v ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge ⟨{x},{y}⟩\in {A}\right)↔\left({x}\in {B}\wedge \exists {y}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩\in {A}\right)$
4 vex ${⊢}{y}\in \mathrm{V}$
5 4 opelresi ${⊢}⟨{x},{y}⟩\in \left({{A}↾}_{{B}}\right)↔\left({x}\in {B}\wedge ⟨{x},{y}⟩\in {A}\right)$
6 5 exbii ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩\in \left({{A}↾}_{{B}}\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge ⟨{x},{y}⟩\in {A}\right)$
7 1 eldm2 ${⊢}{x}\in \mathrm{dom}{A}↔\exists {y}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩\in {A}$
8 7 anbi2i ${⊢}\left({x}\in {B}\wedge {x}\in \mathrm{dom}{A}\right)↔\left({x}\in {B}\wedge \exists {y}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩\in {A}\right)$
9 3 6 8 3bitr4i ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩\in \left({{A}↾}_{{B}}\right)↔\left({x}\in {B}\wedge {x}\in \mathrm{dom}{A}\right)$
10 2 9 bitr2i ${⊢}\left({x}\in {B}\wedge {x}\in \mathrm{dom}{A}\right)↔{x}\in \mathrm{dom}\left({{A}↾}_{{B}}\right)$
11 10 ineqri ${⊢}{B}\cap \mathrm{dom}{A}=\mathrm{dom}\left({{A}↾}_{{B}}\right)$
12 11 eqcomi ${⊢}\mathrm{dom}\left({{A}↾}_{{B}}\right)={B}\cap \mathrm{dom}{A}$