Theorem dmres 5971

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 3434	. . . . 5 ⊢ 𝑥 ∈ V
2	1	eldm2 5850	. . . 4 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵))
3		19.42v 1955	. . . . 5 ⊢ (∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
4		vex 3434	. . . . . . 7 ⊢ 𝑦 ∈ V
5	4	opelresi 5946	. . . . . 6 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
6	5	exbii 1850	. . . . 5 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
7	1	eldm2 5850	. . . . . 6 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
8	7	anbi2i 624	. . . . 5 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
9	3, 6, 8	3bitr4i 303	. . . 4 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴))
10	2, 9	bitr2i 276	. . 3 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ 𝑥 ∈ dom (𝐴 ↾ 𝐵))
11	10	ineqri 4153	. 2 ⊢ (𝐵 ∩ dom 𝐴) = dom (𝐴 ↾ 𝐵)
12	11	eqcomi 2746	1 ⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴)

Syntax hints:   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114   ∩ cin 3889  ⟨cop 4574  dom cdm 5624   ↾ cres 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-xp 5630  df-dm 5634  df-res 5636

This theorem is referenced by:  ssdmres  5972  dmresexg  5973  dmressnsn  5982  eldmeldmressn  5984  relresdm1  5992  imadisj  6039  imainrect  6139  dmresv  6158  resdmres  6190  resdmss  6193  coeq0  6214  resssxp  6228  snres0  6256  funimacnv  6573  fnresdisj  6612  fnres  6619  fresaunres2  6706  nfvres  6872  ssimaex  6919  fnreseql  6994  respreima  7012  fveqressseq  7025  ffvresb  7072  fsnunfv  7135  funfvima  7178  funiunfv  7196  offres  7929  fnwelem  8074  ressuppss  8126  ressuppssdif  8128  frrlem11  8239  frrlem12  8240  smores  8285  smores3  8286  smores2  8287  tz7.44-2  8339  tz7.44-3  8340  frfnom  8367  sbthlem5  9022  sbthlem7  9024  domss2  9067  imafi  9218  ordtypelem4  9429  wdomima2g  9494  r0weon  9925  imadomg  10447  dmaddpi  10804  dmmulpi  10805  ltweuz  13914  dmhashres  14294  limsupgle  15430  fvsetsid  17129  setsdm  17131  setsfun  17132  setsfun0  17133  setsres  17139  lubdm  18306  glbdm  18319  gsumzaddlem  19887  dprdcntz2  20006  lmres  23275  imacmp  23372  qtoptop2  23674  kqdisj  23707  metreslem  24337  setsmstopn  24453  ismbl  25503  mbfres  25621  dvres3a  25891  cpnres  25914  dvlipcn  25971  dvlip2  25972  c1lip3  25976  dvcnvrelem1  25994  dvcvx  25997  dvlog  26628  ltsres  27640  nolesgn2ores  27650  nogesgn1ores  27652  nodense  27670  nosupres  27685  nosupbnd1lem1  27686  nosupbnd2lem1  27693  nosupbnd2  27694  noinfres  27700  noinfbnd1lem1  27701  noinfbnd2lem1  27708  noetasuplem2  27712  noetainflem2  27716  oniso  28277  bdayn0sf1o  28376  uhgrspansubgrlem  29373  trlsegvdeglem4  30308  hlimcaui  31322  ftc2re  34758  dfrdg2  35991  bj-fvsnun2  37586  caures  38095  ssbnd  38123  dmcnvepres  38725  dmuncnvepres  38726  dmxrncnvepres2  38768  mapfzcons1  43163  diophrw  43205  eldioph2lem1  43206  eldioph2lem2  43207  tfsconcatrev  43794  limsupresxr  46212  liminfresxr  46213  fourierdlem93  46645  fouriersw  46677  sssmf  47184  eldmressn  47497  fnresfnco  47501  afvres  47632  afv2res  47699  resinsn  49359  resinsnALT  49360  tposrescnv  49366