Theorem dmres 6013

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 3461	. . . . 5 ⊢ 𝑥 ∈ V
2	1	eldm2 5893	. . . 4 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵))
3		19.42v 1986	. . . . 5 ⊢ (∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
4		vex 3461	. . . . . . 7 ⊢ 𝑦 ∈ V
5	4	opelresi 5988	. . . . . 6 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
6	5	exbii 1881	. . . . 5 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
7	1	eldm2 5893	. . . . . 6 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
8	7	anbi2i 635	. . . . 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 2774	1 ⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴)

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2146   ∩ cin 3905  ⟨cop 4597  dom cdm 5663   ↾ cres 5665

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-xp 5669  df-dm 5673  df-res 5675

This theorem is used by:  ssdmres  6014  dmresexg  6015  dmressnsn  6024  eldmeldmressn  6026  resindm  6031  relresdm1  6037  imadisj  6084  imainrect  6181  dmresv  6201  resdmres  6235  resdmss  6238  coeq0  6259  resssxp  6274  snres0  6303  funimacnv  6621  fnresdisj  6659  fnres  6666  fresaunres2  6754  nfvres  6923  ssimaex  6970  fnreseql  7047  respreima  7065  fveqressseq  7078  ffvresb  7125  fsnunfv  7189  funfvima  7232  funiunfv  7248  offres  7982  fnwelem  8129  ressuppss  8181  ressuppssdif  8183  frrlem11  8295  frrlem12  8296  smores  8341  smores3  8342  smores2  8343  tz7.44-2  8396  tz7.44-3  8397  frfnom  8424  sbthlem5  9082  sbthlem7  9084  domss2  9127  imafi  9278  ordtypelem4  9486  wdomima2g  9551  r0weon  10008  imadomg  10529  dmaddpi  10886  dmmulpi  10887  ltweuz  14011  dmhashres  14391  limsupgle  15548  fvsetsid  17246  setsdm  17248  setsfun  17249  setsfun0  17250  setsres  17256  lubdm  18423  glbdm  18436  gsumzaddlem  20015  dprdcntz2  20134  lmres  23487  imacmp  23584  qtoptop2  23887  kqdisj  23920  metreslem  24550  setsmstopn  24666  ismbl  25716  mbfres  25834  dvres3a  26104  cpnres  26127  dvlipcn  26184  dvlip2  26185  c1lip3  26189  dvcnvrelem1  26207  dvcvx  26210  dvlog  26847  ltsres  27857  nolesgn2ores  27867  nogesgn1ores  27869  nodense  27887  nosupres  27902  nosupbnd1lem1  27903  nosupbnd2lem1  27910  nosupbnd2  27911  noinfres  27917  noinfbnd1lem1  27918  noinfbnd2lem1  27925  noetasuplem2  27929  noetainflem2  27933  oniso  28495  bdayn0sf1o  28594  uhgrspansubgrlem  29674  trlsegvdeglem4  30621  hlimcaui  31635  ftc2re  35026  dfrdg2  36298  bj-fvsnun2  37933  caures  38444  ssbnd  38472  dmcnvepres  39072  dmuncnvepres  39073  dmxrncnvepres2  39115  mapfzcons1  43481  diophrw  43523  eldioph2lem1  43524  eldioph2lem2  43525  tfsconcatrev  44108  limsupresxr  46513  liminfresxr  46514  fourierdlem93  46946  fouriersw  46978  eldmressn  47807  fnresfnco  47811  afvres  47942  afv2res  48009  resinsn  49683  resinsnALT  49684  tposrescnv  49690