Theorem dmres 5858

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 3402	. . . . 5 ⊢ 𝑥 ∈ V
2	1	eldm2 5755	. . . 4 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵))
3		19.42v 1962	. . . . 5 ⊢ (∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
4		vex 3402	. . . . . . 7 ⊢ 𝑦 ∈ V
5	4	opelresi 5844	. . . . . 6 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
6	5	exbii 1855	. . . . 5 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
7	1	eldm2 5755	. . . . . 6 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
8	7	anbi2i 626	. . . . 5 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
9	3, 6, 8	3bitr4i 306	. . . 4 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴))
10	2, 9	bitr2i 279	. . 3 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ 𝑥 ∈ dom (𝐴 ↾ 𝐵))
11	10	ineqri 4105	. 2 ⊢ (𝐵 ∩ dom 𝐴) = dom (𝐴 ↾ 𝐵)
12	11	eqcomi 2745	1 ⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴)

Syntax hints:   ∧ wa 399   = wceq 1543  ∃wex 1787   ∈ wcel 2112   ∩ cin 3852  ⟨cop 4533  dom cdm 5536   ↾ cres 5538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-in 3860  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-br 5040  df-opab 5102  df-xp 5542  df-dm 5546  df-res 5548

This theorem is referenced by:  ssdmres  5859  dmresexg  5860  dmressnsn  5878  eldmeldmressn  5880  imadisj  5933  imainrect  6024  dmresv  6043  resdmres  6075  resdmss  6078  coeq0  6099  resssxp  6113  funimacnv  6439  fnresdisj  6475  fnres  6482  fresaunres2  6569  nfvres  6731  ssimaex  6774  fnreseql  6846  respreima  6864  fveqressseq  6878  ffvresb  6919  fsnunfv  6980  funfvima  7024  funiunfv  7039  offres  7734  fnwelem  7876  ressuppss  7903  ressuppssdif  7905  frrlem11  8015  frrlem12  8016  smores  8067  smores3  8068  smores2  8069  tz7.44-2  8121  tz7.44-3  8122  frfnom  8148  sbthlem5  8738  sbthlem7  8740  domss2  8783  imafiOLD  8947  ordtypelem4  9115  wdomima2g  9180  r0weon  9591  imadomg  10113  dmaddpi  10469  dmmulpi  10470  ltweuz  13499  dmhashres  13872  limsupgle  15003  fvsetsid  16697  setsdm  16699  setsfun  16700  setsfun0  16701  setsres  16707  lubdm  17811  glbdm  17824  gsumzaddlem  19260  dprdcntz2  19379  lmres  22151  imacmp  22248  qtoptop2  22550  kqdisj  22583  metreslem  23214  setsmstopn  23330  ismbl  24377  mbfres  24495  dvres3a  24765  cpnres  24788  dvlipcn  24845  dvlip2  24846  c1lip3  24850  dvcnvrelem1  24868  dvcvx  24871  dvlog  25493  uhgrspansubgrlem  27332  trlsegvdeglem4  28260  hlimcaui  29271  funresdm1  30617  ftc2re  32244  snres0  33344  dfrdg2  33441  sltres  33551  nolesgn2ores  33561  nogesgn1ores  33563  nodense  33581  nosupres  33596  nosupbnd1lem1  33597  nosupbnd2lem1  33604  nosupbnd2  33605  noinfres  33611  noinfbnd1lem1  33612  noinfbnd2lem1  33619  noetasuplem2  33623  noetainflem2  33627  bj-fvsnun2  35111  caures  35604  ssbnd  35632  mapfzcons1  40183  diophrw  40225  eldioph2lem1  40226  eldioph2lem2  40227  dmresss  42388  limsupresxr  42925  liminfresxr  42926  fourierdlem93  43358  fouriersw  43390  sssmf  43889  eldmressn  44146  fnresfnco  44150  afvres  44279  afv2res  44346