Theorem dmres 5913

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 3436	. . . . 5 ⊢ 𝑥 ∈ V
2	1	eldm2 5810	. . . 4 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵))
3		19.42v 1957	. . . . 5 ⊢ (∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
4		vex 3436	. . . . . . 7 ⊢ 𝑦 ∈ V
5	4	opelresi 5899	. . . . . 6 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
6	5	exbii 1850	. . . . 5 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
7	1	eldm2 5810	. . . . . 6 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
8	7	anbi2i 623	. . . . 5 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
9	3, 6, 8	3bitr4i 303	. . . 4 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴))
10	2, 9	bitr2i 275	. . 3 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ 𝑥 ∈ dom (𝐴 ↾ 𝐵))
11	10	ineqri 4138	. 2 ⊢ (𝐵 ∩ dom 𝐴) = dom (𝐴 ↾ 𝐵)
12	11	eqcomi 2747	1 ⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴)

Syntax hints:   ∧ wa 396   = wceq 1539  ∃wex 1782   ∈ wcel 2106   ∩ cin 3886  ⟨cop 4567  dom cdm 5589   ↾ cres 5591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-opab 5137  df-xp 5595  df-dm 5599  df-res 5601

This theorem is referenced by:  ssdmres  5914  dmresexg  5915  dmressnsn  5933  eldmeldmressn  5935  imadisj  5988  imainrect  6084  dmresv  6103  resdmres  6135  resdmss  6138  coeq0  6159  resssxp  6173  funimacnv  6515  fnresdisj  6552  fnres  6559  fresaunres2  6646  nfvres  6810  ssimaex  6853  fnreseql  6925  respreima  6943  fveqressseq  6957  ffvresb  6998  fsnunfv  7059  funfvima  7106  funiunfv  7121  offres  7826  fnwelem  7972  ressuppss  7999  ressuppssdif  8001  frrlem11  8112  frrlem12  8113  smores  8183  smores3  8184  smores2  8185  tz7.44-2  8238  tz7.44-3  8239  frfnom  8266  sbthlem5  8874  sbthlem7  8876  domss2  8923  imafiALT  9112  ordtypelem4  9280  wdomima2g  9345  r0weon  9768  imadomg  10290  dmaddpi  10646  dmmulpi  10647  ltweuz  13681  dmhashres  14055  limsupgle  15186  fvsetsid  16869  setsdm  16871  setsfun  16872  setsfun0  16873  setsres  16879  lubdm  18069  glbdm  18082  gsumzaddlem  19522  dprdcntz2  19641  lmres  22451  imacmp  22548  qtoptop2  22850  kqdisj  22883  metreslem  23515  setsmstopn  23633  ismbl  24690  mbfres  24808  dvres3a  25078  cpnres  25101  dvlipcn  25158  dvlip2  25159  c1lip3  25163  dvcnvrelem1  25181  dvcvx  25184  dvlog  25806  uhgrspansubgrlem  27657  trlsegvdeglem4  28587  hlimcaui  29598  funresdm1  30944  ftc2re  32578  snres0  33675  dfrdg2  33771  sltres  33865  nolesgn2ores  33875  nogesgn1ores  33877  nodense  33895  nosupres  33910  nosupbnd1lem1  33911  nosupbnd2lem1  33918  nosupbnd2  33919  noinfres  33925  noinfbnd1lem1  33926  noinfbnd2lem1  33933  noetasuplem2  33937  noetainflem2  33941  bj-fvsnun2  35427  caures  35918  ssbnd  35946  mapfzcons1  40539  diophrw  40581  eldioph2lem1  40582  eldioph2lem2  40583  dmresss  42774  limsupresxr  43307  liminfresxr  43308  fourierdlem93  43740  fouriersw  43772  sssmf  44274  eldmressn  44531  fnresfnco  44535  afvres  44664  afv2res  44731