Theorem dmres 5902

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 3426	. . . . 5 ⊢ 𝑥 ∈ V
2	1	eldm2 5799	. . . 4 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵))
3		19.42v 1958	. . . . 5 ⊢ (∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
4		vex 3426	. . . . . . 7 ⊢ 𝑦 ∈ V
5	4	opelresi 5888	. . . . . 6 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
6	5	exbii 1851	. . . . 5 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
7	1	eldm2 5799	. . . . . 6 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
8	7	anbi2i 622	. . . . 5 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
9	3, 6, 8	3bitr4i 302	. . . 4 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴))
10	2, 9	bitr2i 275	. . 3 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ 𝑥 ∈ dom (𝐴 ↾ 𝐵))
11	10	ineqri 4135	. 2 ⊢ (𝐵 ∩ dom 𝐴) = dom (𝐴 ↾ 𝐵)
12	11	eqcomi 2747	1 ⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴)

Syntax hints:   ∧ wa 395   = wceq 1539  ∃wex 1783   ∈ wcel 2108   ∩ cin 3882  ⟨cop 4564  dom cdm 5580   ↾ cres 5582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-xp 5586  df-dm 5590  df-res 5592

This theorem is referenced by:  ssdmres  5903  dmresexg  5904  dmressnsn  5922  eldmeldmressn  5924  imadisj  5977  imainrect  6073  dmresv  6092  resdmres  6124  resdmss  6127  coeq0  6148  resssxp  6162  funimacnv  6499  fnresdisj  6536  fnres  6543  fresaunres2  6630  nfvres  6792  ssimaex  6835  fnreseql  6907  respreima  6925  fveqressseq  6939  ffvresb  6980  fsnunfv  7041  funfvima  7088  funiunfv  7103  offres  7799  fnwelem  7943  ressuppss  7970  ressuppssdif  7972  frrlem11  8083  frrlem12  8084  smores  8154  smores3  8155  smores2  8156  tz7.44-2  8209  tz7.44-3  8210  frfnom  8236  sbthlem5  8827  sbthlem7  8829  domss2  8872  imafiALT  9042  ordtypelem4  9210  wdomima2g  9275  r0weon  9699  imadomg  10221  dmaddpi  10577  dmmulpi  10578  ltweuz  13609  dmhashres  13983  limsupgle  15114  fvsetsid  16797  setsdm  16799  setsfun  16800  setsfun0  16801  setsres  16807  lubdm  17984  glbdm  17997  gsumzaddlem  19437  dprdcntz2  19556  lmres  22359  imacmp  22456  qtoptop2  22758  kqdisj  22791  metreslem  23423  setsmstopn  23539  ismbl  24595  mbfres  24713  dvres3a  24983  cpnres  25006  dvlipcn  25063  dvlip2  25064  c1lip3  25068  dvcnvrelem1  25086  dvcvx  25089  dvlog  25711  uhgrspansubgrlem  27560  trlsegvdeglem4  28488  hlimcaui  29499  funresdm1  30845  ftc2re  32478  snres0  33577  dfrdg2  33677  sltres  33792  nolesgn2ores  33802  nogesgn1ores  33804  nodense  33822  nosupres  33837  nosupbnd1lem1  33838  nosupbnd2lem1  33845  nosupbnd2  33846  noinfres  33852  noinfbnd1lem1  33853  noinfbnd2lem1  33860  noetasuplem2  33864  noetainflem2  33868  bj-fvsnun2  35354  caures  35845  ssbnd  35873  mapfzcons1  40455  diophrw  40497  eldioph2lem1  40498  eldioph2lem2  40499  dmresss  42663  limsupresxr  43197  liminfresxr  43198  fourierdlem93  43630  fouriersw  43662  sssmf  44161  eldmressn  44418  fnresfnco  44422  afvres  44551  afv2res  44618