Theorem dmres 6012

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 3467	. . . . 5 ⊢ 𝑥 ∈ V
2	1	eldm2 5892	. . . 4 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵))
3		19.42v 1980	. . . . 5 ⊢ (∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
4		vex 3467	. . . . . . 7 ⊢ 𝑦 ∈ V
5	4	opelresi 5987	. . . . . 6 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
6	5	exbii 1875	. . . . 5 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
7	1	eldm2 5892	. . . . . 6 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
8	7	anbi2i 634	. . . . 5 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
9	3, 6, 8	3bitr4i 306	. . . 4 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴))
10	2, 9	bitr2i 279	. . 3 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ 𝑥 ∈ dom (𝐴 ↾ 𝐵))
11	10	ineqri 4173	. 2 ⊢ (𝐵 ∩ dom 𝐴) = dom (𝐴 ↾ 𝐵)
12	11	eqcomi 2778	1 ⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴)

Syntax hints:   ∧ wa 400   = wceq 1567  ∃wex 1806   ∈ wcel 2149   ∩ cin 3912  ⟨cop 4600  dom cdm 5662   ↾ cres 5664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-opab 5178  df-xp 5668  df-dm 5672  df-res 5674

This theorem is referenced by:  ssdmres  6013  dmresexg  6014  dmressnsn  6023  eldmeldmressn  6025  resindm  6030  relresdm1  6036  imadisj  6083  imainrect  6180  dmresv  6200  resdmres  6234  resdmss  6237  coeq0  6258  resssxp  6272  snres0  6300  funimacnv  6618  fnresdisj  6656  fnres  6663  fresaunres2  6751  nfvres  6920  ssimaex  6967  fnreseql  7044  respreima  7062  fveqressseq  7075  ffvresb  7122  fsnunfv  7186  funfvima  7229  funiunfv  7247  offres  7980  fnwelem  8127  ressuppss  8179  ressuppssdif  8181  frrlem11  8293  frrlem12  8294  smores  8339  smores3  8340  smores2  8341  tz7.44-2  8394  tz7.44-3  8395  frfnom  8422  sbthlem5  9079  sbthlem7  9081  domss2  9124  imafi  9275  ordtypelem4  9483  wdomima2g  9548  r0weon  9996  imadomg  10518  dmaddpi  10875  dmmulpi  10876  ltweuz  13997  dmhashres  14377  limsupgle  15528  fvsetsid  17228  setsdm  17230  setsfun  17231  setsfun0  17232  setsres  17238  lubdm  18405  glbdm  18418  gsumzaddlem  19991  dprdcntz2  20110  lmres  23426  imacmp  23523  qtoptop2  23825  kqdisj  23858  metreslem  24488  setsmstopn  24604  ismbl  25654  mbfres  25772  dvres3a  26042  cpnres  26065  dvlipcn  26122  dvlip2  26123  c1lip3  26127  dvcnvrelem1  26145  dvcvx  26148  dvlog  26782  ltsres  27792  nolesgn2ores  27802  nogesgn1ores  27804  nodense  27822  nosupres  27837  nosupbnd1lem1  27838  nosupbnd2lem1  27845  nosupbnd2  27846  noinfres  27852  noinfbnd1lem1  27853  noinfbnd2lem1  27860  noetasuplem2  27864  noetainflem2  27868  oniso  28430  bdayn0sf1o  28529  uhgrspansubgrlem  29581  trlsegvdeglem4  30515  hlimcaui  31529  ftc2re  34930  dfrdg2  36218  bj-fvsnun2  37822  caures  38333  ssbnd  38361  dmcnvepres  38963  dmuncnvepres  38964  dmxrncnvepres2  39006  mapfzcons1  43374  diophrw  43416  eldioph2lem1  43417  eldioph2lem2  43418  tfsconcatrev  44001  limsupresxr  46406  liminfresxr  46407  fourierdlem93  46839  fouriersw  46871  eldmressn  47697  fnresfnco  47701  afvres  47832  afv2res  47899  resinsn  49569  resinsnALT  49570  tposrescnv  49576