Theorem dmres 6031

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 3481	. . . . 5 ⊢ 𝑥 ∈ V
2	1	eldm2 5914	. . . 4 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵))
3		19.42v 1950	. . . . 5 ⊢ (∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
4		vex 3481	. . . . . . 7 ⊢ 𝑦 ∈ V
5	4	opelresi 6007	. . . . . 6 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
6	5	exbii 1844	. . . . 5 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
7	1	eldm2 5914	. . . . . 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 4219	. 2 ⊢ (𝐵 ∩ dom 𝐴) = dom (𝐴 ↾ 𝐵)
12	11	eqcomi 2743	1 ⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴)

Syntax hints:   ∧ wa 395   = wceq 1536  ∃wex 1775   ∈ wcel 2105   ∩ cin 3961  ⟨cop 4636  dom cdm 5688   ↾ cres 5690

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-xp 5694  df-dm 5698  df-res 5700

This theorem is referenced by:  ssdmres  6032  dmresexg  6033  dmressnsn  6042  eldmeldmressn  6044  relresdm1  6052  imadisj  6099  imainrect  6202  dmresv  6221  resdmres  6253  resdmss  6256  coeq0  6276  resssxp  6291  snres0  6319  funimacnv  6648  fnresdisj  6688  fnres  6695  fresaunres2  6780  nfvres  6947  ssimaex  6993  fnreseql  7067  respreima  7085  fveqressseq  7098  ffvresb  7144  fsnunfv  7206  funfvima  7249  funiunfv  7267  offres  8006  fnwelem  8154  ressuppss  8206  ressuppssdif  8208  frrlem11  8319  frrlem12  8320  smores  8390  smores3  8391  smores2  8392  tz7.44-2  8445  tz7.44-3  8446  frfnom  8473  sbthlem5  9125  sbthlem7  9127  domss2  9174  imafi  9350  ordtypelem4  9558  wdomima2g  9623  r0weon  10049  imadomg  10571  dmaddpi  10927  dmmulpi  10928  ltweuz  13998  dmhashres  14376  limsupgle  15509  fvsetsid  17201  setsdm  17203  setsfun  17204  setsfun0  17205  setsres  17211  lubdm  18408  glbdm  18421  gsumzaddlem  19953  dprdcntz2  20072  lmres  23323  imacmp  23420  qtoptop2  23722  kqdisj  23755  metreslem  24387  setsmstopn  24505  ismbl  25574  mbfres  25692  dvres3a  25963  cpnres  25987  dvlipcn  26047  dvlip2  26048  c1lip3  26052  dvcnvrelem1  26070  dvcvx  26073  dvlog  26707  sltres  27721  nolesgn2ores  27731  nogesgn1ores  27733  nodense  27751  nosupres  27766  nosupbnd1lem1  27767  nosupbnd2lem1  27774  nosupbnd2  27775  noinfres  27781  noinfbnd1lem1  27782  noinfbnd2lem1  27789  noetasuplem2  27793  noetainflem2  27797  uhgrspansubgrlem  29321  trlsegvdeglem4  30251  hlimcaui  31264  ftc2re  34591  dfrdg2  35776  bj-fvsnun2  37238  caures  37746  ssbnd  37774  mapfzcons1  42704  diophrw  42746  eldioph2lem1  42747  eldioph2lem2  42748  tfsconcatrev  43337  limsupresxr  45721  liminfresxr  45722  fourierdlem93  46154  fouriersw  46186  sssmf  46693  eldmressn  46986  fnresfnco  46990  afvres  47121  afv2res  47188