Theorem dmres 6001

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

Syntax hints:   ∧ wa 396   = wceq 1541  ∃wex 1781   ∈ wcel 2106   ∩ cin 3946  ⟨cop 4633  dom cdm 5675   ↾ cres 5677

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-xp 5681  df-dm 5685  df-res 5687

This theorem is referenced by:  ssdmres  6002  dmresexg  6003  dmressnsn  6021  eldmeldmressn  6023  relresdm1  6031  imadisj  6076  imainrect  6177  dmresv  6196  resdmres  6228  resdmss  6231  coeq0  6251  resssxp  6266  snres0  6294  funimacnv  6626  fnresdisj  6667  fnres  6674  fresaunres2  6760  nfvres  6929  ssimaex  6973  fnreseql  7046  respreima  7064  fveqressseq  7078  ffvresb  7120  fsnunfv  7181  funfvima  7228  funiunfv  7243  offres  7966  fnwelem  8113  ressuppss  8164  ressuppssdif  8166  frrlem11  8277  frrlem12  8278  smores  8348  smores3  8349  smores2  8350  tz7.44-2  8403  tz7.44-3  8404  frfnom  8431  sbthlem5  9083  sbthlem7  9085  domss2  9132  imafiALT  9341  ordtypelem4  9512  wdomima2g  9577  r0weon  10003  imadomg  10525  dmaddpi  10881  dmmulpi  10882  ltweuz  13922  dmhashres  14297  limsupgle  15417  fvsetsid  17097  setsdm  17099  setsfun  17100  setsfun0  17101  setsres  17107  lubdm  18300  glbdm  18313  gsumzaddlem  19783  dprdcntz2  19902  lmres  22795  imacmp  22892  qtoptop2  23194  kqdisj  23227  metreslem  23859  setsmstopn  23977  ismbl  25034  mbfres  25152  dvres3a  25422  cpnres  25445  dvlipcn  25502  dvlip2  25503  c1lip3  25507  dvcnvrelem1  25525  dvcvx  25528  dvlog  26150  sltres  27154  nolesgn2ores  27164  nogesgn1ores  27166  nodense  27184  nosupres  27199  nosupbnd1lem1  27200  nosupbnd2lem1  27207  nosupbnd2  27208  noinfres  27214  noinfbnd1lem1  27215  noinfbnd2lem1  27222  noetasuplem2  27226  noetainflem2  27230  uhgrspansubgrlem  28536  trlsegvdeglem4  29465  hlimcaui  30476  ftc2re  33598  dfrdg2  34755  bj-fvsnun2  36125  caures  36616  ssbnd  36644  mapfzcons1  41440  diophrw  41482  eldioph2lem1  41483  eldioph2lem2  41484  tfsconcatrev  42083  dmresss  43918  limsupresxr  44468  liminfresxr  44469  fourierdlem93  44901  fouriersw  44933  sssmf  45440  eldmressn  45733  fnresfnco  45737  afvres  45866  afv2res  45933