Theorem dmres 6041

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 3492	. . . . 5 ⊢ 𝑥 ∈ V
2	1	eldm2 5926	. . . 4 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵))
3		19.42v 1953	. . . . 5 ⊢ (∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
4		vex 3492	. . . . . . 7 ⊢ 𝑦 ∈ V
5	4	opelresi 6017	. . . . . 6 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
6	5	exbii 1846	. . . . 5 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
7	1	eldm2 5926	. . . . . 6 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
8	7	anbi2i 622	. . . . 5 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
9	3, 6, 8	3bitr4i 303	. . . 4 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴))
10	2, 9	bitr2i 276	. . 3 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ 𝑥 ∈ dom (𝐴 ↾ 𝐵))
11	10	ineqri 4233	. 2 ⊢ (𝐵 ∩ dom 𝐴) = dom (𝐴 ↾ 𝐵)
12	11	eqcomi 2749	1 ⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴)

Syntax hints:   ∧ wa 395   = wceq 1537  ∃wex 1777   ∈ wcel 2108   ∩ cin 3975  ⟨cop 4654  dom cdm 5700   ↾ cres 5702

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-xp 5706  df-dm 5710  df-res 5712

This theorem is referenced by:  ssdmres  6042  dmresexg  6043  dmressnsn  6052  eldmeldmressn  6054  relresdm1  6062  imadisj  6109  imainrect  6212  dmresv  6231  resdmres  6263  resdmss  6266  coeq0  6286  resssxp  6301  snres0  6329  funimacnv  6659  fnresdisj  6700  fnres  6707  fresaunres2  6793  nfvres  6961  ssimaex  7007  fnreseql  7081  respreima  7099  fveqressseq  7113  ffvresb  7159  fsnunfv  7221  funfvima  7267  funiunfv  7285  offres  8024  fnwelem  8172  ressuppss  8224  ressuppssdif  8226  frrlem11  8337  frrlem12  8338  smores  8408  smores3  8409  smores2  8410  tz7.44-2  8463  tz7.44-3  8464  frfnom  8491  sbthlem5  9153  sbthlem7  9155  domss2  9202  imafi  9381  ordtypelem4  9590  wdomima2g  9655  r0weon  10081  imadomg  10603  dmaddpi  10959  dmmulpi  10960  ltweuz  14012  dmhashres  14390  limsupgle  15523  fvsetsid  17215  setsdm  17217  setsfun  17218  setsfun0  17219  setsres  17225  lubdm  18421  glbdm  18434  gsumzaddlem  19963  dprdcntz2  20082  lmres  23329  imacmp  23426  qtoptop2  23728  kqdisj  23761  metreslem  24393  setsmstopn  24511  ismbl  25580  mbfres  25698  dvres3a  25969  cpnres  25993  dvlipcn  26053  dvlip2  26054  c1lip3  26058  dvcnvrelem1  26076  dvcvx  26079  dvlog  26711  sltres  27725  nolesgn2ores  27735  nogesgn1ores  27737  nodense  27755  nosupres  27770  nosupbnd1lem1  27771  nosupbnd2lem1  27778  nosupbnd2  27779  noinfres  27785  noinfbnd1lem1  27786  noinfbnd2lem1  27793  noetasuplem2  27797  noetainflem2  27801  uhgrspansubgrlem  29325  trlsegvdeglem4  30255  hlimcaui  31268  ftc2re  34575  dfrdg2  35759  bj-fvsnun2  37222  caures  37720  ssbnd  37748  mapfzcons1  42673  diophrw  42715  eldioph2lem1  42716  eldioph2lem2  42717  tfsconcatrev  43310  limsupresxr  45687  liminfresxr  45688  fourierdlem93  46120  fouriersw  46152  sssmf  46659  eldmressn  46952  fnresfnco  46956  afvres  47087  afv2res  47154