Theorem dmres 6011

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 3459	. . . . 5 ⊢ 𝑥 ∈ V
2	1	eldm2 5891	. . . 4 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵))
3		19.42v 1983	. . . . 5 ⊢ (∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
4		vex 3459	. . . . . . 7 ⊢ 𝑦 ∈ V
5	4	opelresi 5986	. . . . . 6 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
6	5	exbii 1878	. . . . 5 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
7	1	eldm2 5891	. . . . . 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 4165	. 2 ⊢ (𝐵 ∩ dom 𝐴) = dom (𝐴 ↾ 𝐵)
12	11	eqcomi 2772	1 ⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴)

Syntax hints:   ∧ wa 400   = wceq 1570  ∃wex 1809   ∈ wcel 2143   ∩ cin 3904  ⟨cop 4595  dom cdm 5661   ↾ cres 5663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174  df-xp 5667  df-dm 5671  df-res 5673

This theorem is referenced by:  ssdmres  6012  dmresexg  6013  dmressnsn  6022  eldmeldmressn  6024  resindm  6029  relresdm1  6035  imadisj  6082  imainrect  6179  dmresv  6199  resdmres  6233  resdmss  6236  coeq0  6257  resssxp  6271  snres0  6299  funimacnv  6617  fnresdisj  6655  fnres  6662  fresaunres2  6750  nfvres  6919  ssimaex  6966  fnreseql  7043  respreima  7061  fveqressseq  7074  ffvresb  7121  fsnunfv  7185  funfvima  7228  funiunfv  7246  offres  7976  fnwelem  8123  ressuppss  8175  ressuppssdif  8177  frrlem11  8289  frrlem12  8290  smores  8335  smores3  8336  smores2  8337  tz7.44-2  8390  tz7.44-3  8391  frfnom  8418  sbthlem5  9075  sbthlem7  9077  domss2  9120  imafi  9271  ordtypelem4  9479  wdomima2g  9544  r0weon  9992  imadomg  10513  dmaddpi  10870  dmmulpi  10871  ltweuz  13993  dmhashres  14373  limsupgle  15524  fvsetsid  17223  setsdm  17225  setsfun  17226  setsfun0  17227  setsres  17233  lubdm  18400  glbdm  18413  gsumzaddlem  19986  dprdcntz2  20105  lmres  23457  imacmp  23554  qtoptop2  23856  kqdisj  23889  metreslem  24519  setsmstopn  24635  ismbl  25685  mbfres  25803  dvres3a  26073  cpnres  26096  dvlipcn  26153  dvlip2  26154  c1lip3  26158  dvcnvrelem1  26176  dvcvx  26179  dvlog  26816  ltsres  27826  nolesgn2ores  27836  nogesgn1ores  27838  nodense  27856  nosupres  27871  nosupbnd1lem1  27872  nosupbnd2lem1  27879  nosupbnd2  27880  noinfres  27886  noinfbnd1lem1  27887  noinfbnd2lem1  27894  noetasuplem2  27898  noetainflem2  27902  oniso  28464  bdayn0sf1o  28563  uhgrspansubgrlem  29640  trlsegvdeglem4  30574  hlimcaui  31588  ftc2re  34985  dfrdg2  36285  bj-fvsnun2  37900  caures  38411  ssbnd  38439  dmcnvepres  39039  dmuncnvepres  39040  dmxrncnvepres2  39082  mapfzcons1  43448  diophrw  43490  eldioph2lem1  43491  eldioph2lem2  43492  tfsconcatrev  44075  limsupresxr  46480  liminfresxr  46481  fourierdlem93  46913  fouriersw  46945  eldmressn  47774  fnresfnco  47778  afvres  47909  afv2res  47976  resinsn  49650  resinsnALT  49651  tposrescnv  49657