Theorem dmres 5956

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 3440	. . . . 5 ⊢ 𝑥 ∈ V
2	1	eldm2 5836	. . . 4 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵))
3		19.42v 1954	. . . . 5 ⊢ (∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
4		vex 3440	. . . . . . 7 ⊢ 𝑦 ∈ V
5	4	opelresi 5931	. . . . . 6 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
6	5	exbii 1849	. . . . 5 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
7	1	eldm2 5836	. . . . . 6 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
8	7	anbi2i 623	. . . . 5 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
9	3, 6, 8	3bitr4i 303	. . . 4 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴))
10	2, 9	bitr2i 276	. . 3 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ 𝑥 ∈ dom (𝐴 ↾ 𝐵))
11	10	ineqri 4157	. 2 ⊢ (𝐵 ∩ dom 𝐴) = dom (𝐴 ↾ 𝐵)
12	11	eqcomi 2740	1 ⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴)

Syntax hints:   ∧ wa 395   = wceq 1541  ∃wex 1780   ∈ wcel 2111   ∩ cin 3896  ⟨cop 4577  dom cdm 5611   ↾ cres 5613

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pr 5365

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-br 5087  df-opab 5149  df-xp 5617  df-dm 5621  df-res 5623

This theorem is referenced by:  ssdmres  5957  dmresexg  5958  dmressnsn  5967  eldmeldmressn  5969  relresdm1  5977  imadisj  6024  imainrect  6123  dmresv  6142  resdmres  6174  resdmss  6177  coeq0  6198  resssxp  6212  snres0  6240  funimacnv  6557  fnresdisj  6596  fnres  6603  fresaunres2  6690  nfvres  6855  ssimaex  6902  fnreseql  6976  respreima  6994  fveqressseq  7007  ffvresb  7053  fsnunfv  7116  funfvima  7159  funiunfv  7177  offres  7910  fnwelem  8056  ressuppss  8108  ressuppssdif  8110  frrlem11  8221  frrlem12  8222  smores  8267  smores3  8268  smores2  8269  tz7.44-2  8321  tz7.44-3  8322  frfnom  8349  sbthlem5  8999  sbthlem7  9001  domss2  9044  imafi  9194  ordtypelem4  9402  wdomima2g  9467  r0weon  9898  imadomg  10420  dmaddpi  10776  dmmulpi  10777  ltweuz  13863  dmhashres  14243  limsupgle  15379  fvsetsid  17074  setsdm  17076  setsfun  17077  setsfun0  17078  setsres  17084  lubdm  18250  glbdm  18263  gsumzaddlem  19828  dprdcntz2  19947  lmres  23210  imacmp  23307  qtoptop2  23609  kqdisj  23642  metreslem  24272  setsmstopn  24388  ismbl  25449  mbfres  25567  dvres3a  25837  cpnres  25861  dvlipcn  25921  dvlip2  25922  c1lip3  25926  dvcnvrelem1  25944  dvcvx  25947  dvlog  26582  sltres  27596  nolesgn2ores  27606  nogesgn1ores  27608  nodense  27626  nosupres  27641  nosupbnd1lem1  27642  nosupbnd2lem1  27649  nosupbnd2  27650  noinfres  27656  noinfbnd1lem1  27657  noinfbnd2lem1  27664  noetasuplem2  27668  noetainflem2  27672  onsiso  28200  bdayn0sf1o  28290  uhgrspansubgrlem  29263  trlsegvdeglem4  30195  hlimcaui  31208  ftc2re  34603  dfrdg2  35829  bj-fvsnun2  37290  caures  37800  ssbnd  37828  mapfzcons1  42750  diophrw  42792  eldioph2lem1  42793  eldioph2lem2  42794  tfsconcatrev  43381  limsupresxr  45804  liminfresxr  45805  fourierdlem93  46237  fouriersw  46269  sssmf  46776  eldmressn  47068  fnresfnco  47072  afvres  47203  afv2res  47270  resinsn  48903  resinsnALT  48904  tposrescnv  48910