Theorem dmres 5616

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 3390	. . . . 5 ⊢ 𝑥 ∈ V
2	1	eldm2 5517	. . . 4 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵))
3		19.41v 2039	. . . . 5 ⊢ (∃𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ (∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
4		vex 3390	. . . . . . 7 ⊢ 𝑦 ∈ V
5	4	opelres 5599	. . . . . 6 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
6	5	exbii 1933	. . . . 5 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ ∃𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
7	1	eldm2 5517	. . . . . 6 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
8	7	anbi1i 612	. . . . 5 ⊢ ((𝑥 ∈ dom 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ (∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
9	3, 6, 8	3bitr4i 294	. . . 4 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ dom 𝐴 ∧ 𝑥 ∈ 𝐵))
10	2, 9	bitr2i 267	. . 3 ⊢ ((𝑥 ∈ dom 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ dom (𝐴 ↾ 𝐵))
11	10	ineqri 3999	. 2 ⊢ (dom 𝐴 ∩ 𝐵) = dom (𝐴 ↾ 𝐵)
12		incom 3998	. 2 ⊢ (dom 𝐴 ∩ 𝐵) = (𝐵 ∩ dom 𝐴)
13	11, 12	eqtr3i 2826	1 ⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴)

Syntax hints:   ∧ wa 384   = wceq 1637  ∃wex 1859   ∈ wcel 2155   ∩ cin 3762  ⟨cop 4370  dom cdm 5305   ↾ cres 5307

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781  ax-sep 4968  ax-nul 4977  ax-pr 5090

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-ral 3097  df-rex 3098  df-rab 3101  df-v 3389  df-dif 3766  df-un 3768  df-in 3770  df-ss 3777  df-nul 4111  df-if 4274  df-sn 4365  df-pr 4367  df-op 4371  df-br 4838  df-opab 4900  df-xp 5311  df-dm 5315  df-res 5317

This theorem is referenced by:  ssdmres  5617  dmresexg  5618  dmressnsn  5637  eldmeldmressn  5639  imadisj  5688  imainrect  5780  dmresv  5798  resdmres  5833  coeq0  5852  funimacnv  6175  fnresdisj  6206  fnres  6212  fresaunres2  6285  nfvres  6438  ssimaex  6478  fnreseql  6543  respreima  6560  fveqressseq  6571  ffvresb  6610  fsnunfv  6672  funfvima  6711  funiunfv  6724  offres  7387  fnwelem  7520  ressuppss  7542  ressuppssdif  7544  smores  7679  smores3  7680  smores2  7681  tz7.44-2  7733  tz7.44-3  7734  frfnom  7760  sbthlem5  8307  sbthlem7  8309  domss2  8352  imafi  8492  ordtypelem4  8659  wdomima2g  8724  r0weon  9112  imadomg  9635  dmaddpi  9991  dmmulpi  9992  ltweuz  12978  dmhashres  13343  limsupgle  14425  fvsetsid  16095  setsdm  16097  setsfun  16098  setsfun0  16099  setsres  16106  lubdm  17178  glbdm  17191  gsumzaddlem  18516  dprdcntz2  18633  lmres  21312  imacmp  21408  qtoptop2  21710  kqdisj  21743  metreslem  22374  setsmstopn  22490  ismbl  23501  mbfres  23619  dvres3a  23886  cpnres  23908  dvlipcn  23965  dvlip2  23966  c1lip3  23970  dvcnvrelem1  23988  dvcvx  23991  dvlog  24605  uhgrspansubgrlem  26392  wlkres  26789  trlsegvdeglem4  27390  hlimcaui  28415  funresdm1  29735  ftc2re  30995  dfrdg2  32015  sltres  32130  nolesgn2ores  32140  nodense  32157  nosupres  32168  nosupbnd1lem1  32169  nosupbnd2lem1  32176  nosupbnd2  32177  caures  33861  ssbnd  33892  mapfzcons1  37776  diophrw  37818  eldioph2lem1  37819  eldioph2lem2  37820  rp-imass  38559  dmresss  39914  limsupresxr  40472  liminfresxr  40473  fourierdlem93  40889  fouriersw  40921  sssmf  41423  eldmressn  41650  fnresfnco  41654  afvres  41755  afv2res  41822  setrec2lem1  43002