Theorem dmres 5454

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

Assertion

Ref	Expression
dmres	⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴)

Proof of Theorem dmres

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3234	. . . . 5 ⊢ 𝑥 ∈ V
2	1	eldm2 5354	. . . 4 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵))
3		19.41v 1917	. . . . 5 ⊢ (∃𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ (∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
4		vex 3234	. . . . . . 7 ⊢ 𝑦 ∈ V
5	4	opelres 5436	. . . . . 6 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
6	5	exbii 1814	. . . . 5 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ ∃𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
7	1	eldm2 5354	. . . . . 6 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
8	7	anbi1i 731	. . . . 5 ⊢ ((𝑥 ∈ dom 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ (∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
9	3, 6, 8	3bitr4i 292	. . . 4 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ dom 𝐴 ∧ 𝑥 ∈ 𝐵))
10	2, 9	bitr2i 265	. . 3 ⊢ ((𝑥 ∈ dom 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ dom (𝐴 ↾ 𝐵))
11	10	ineqri 3839	. 2 ⊢ (dom 𝐴 ∩ 𝐵) = dom (𝐴 ↾ 𝐵)
12		incom 3838	. 2 ⊢ (dom 𝐴 ∩ 𝐵) = (𝐵 ∩ dom 𝐴)
13	11, 12	eqtr3i 2675	1 ⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴)

Syntax hints:   ∧ wa 383   = wceq 1523  ∃wex 1744   ∈ wcel 2030   ∩ cin 3606  ⟨cop 4216  dom cdm 5143   ↾ cres 5145

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-opab 4746  df-xp 5149  df-dm 5153  df-res 5155

This theorem is referenced by:  ssdmres  5455  dmresexg  5456  dmressnsn  5473  eldmeldmressn  5475  imadisj  5519  imainrect  5610  dmresv  5628  resdmres  5663  coeq0  5682  funimacnv  6008  fnresdisj  6039  fnres  6045  fresaunres2  6114  nfvres  6262  ssimaex  6302  fnreseql  6367  respreima  6384  fveqressseq  6395  ffvresb  6434  fsnunfv  6494  funfvima  6532  funiunfv  6546  offres  7205  fnwelem  7337  ressuppss  7359  ressuppssdif  7361  smores  7494  smores3  7495  smores2  7496  tz7.44-2  7548  tz7.44-3  7549  frfnom  7575  sbthlem5  8115  sbthlem7  8117  domss2  8160  imafi  8300  ordtypelem4  8467  wdomima2g  8532  r0weon  8873  imadomg  9394  dmaddpi  9750  dmmulpi  9751  ltweuz  12800  dmhashres  13169  limsupgle  14252  fvsetsid  15937  setsdm  15939  setsfun  15940  setsfun0  15941  setsres  15948  lubdm  17026  glbdm  17039  gsumzaddlem  18367  dprdcntz2  18483  lmres  21152  imacmp  21248  qtoptop2  21550  kqdisj  21583  metreslem  22214  setsmstopn  22330  ismbl  23340  mbfres  23456  dvres3a  23723  cpnres  23745  dvlipcn  23802  dvlip2  23803  c1lip3  23807  dvcnvrelem1  23825  dvcvx  23828  dvlog  24442  uhgrspansubgrlem  26227  wlkres  26623  trlsegvdeglem4  27201  hlimcaui  28221  funresdm1  29542  ftc2re  30804  dfrdg2  31825  sltres  31940  nolesgn2ores  31950  nodense  31967  nosupres  31978  nosupbnd1lem1  31979  nosupbnd2lem1  31986  nosupbnd2  31987  caures  33686  ssbnd  33717  mapfzcons1  37597  diophrw  37639  eldioph2lem1  37640  eldioph2lem2  37641  rp-imass  38382  dmresss  39750  limsupresxr  40316  liminfresxr  40317  fourierdlem93  40734  fouriersw  40766  sssmf  41268  eldmressn  41524  fnresfnco  41527  afvres  41573  setrec2lem1  42765