Theorem dmres 6002

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 3454	. . . . 5 ⊢ 𝑥 ∈ V
2	1	eldm2 5882	. . . 4 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵))
3		19.42v 1985	. . . . 5 ⊢ (∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
4		vex 3454	. . . . . . 7 ⊢ 𝑦 ∈ V
5	4	opelresi 5977	. . . . . 6 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
6	5	exbii 1880	. . . . 5 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
7	1	eldm2 5882	. . . . . 6 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
8	7	anbi2i 635	. . . . 5 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
9	3, 6, 8	3bitr4i 306	. . . 4 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴))
10	2, 9	bitr2i 279	. . 3 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ 𝑥 ∈ dom (𝐴 ↾ 𝐵))
11	10	ineqri 4109	. 2 ⊢ (𝐵 ∩ dom 𝐴) = dom (𝐴 ↾ 𝐵)
12	11	eqcomi 2769	1 ⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴)

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1569  ∃wex 1811   ∈ wcel 2144   ∩ cin 4089  ⟨cop 4834  dom cdm 5650   ↾ cres 5652

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-xp 5656  df-dm 5660  df-res 5662

This theorem is used by:  ssdmres  6003  dmresexg  6004  dmressnsn  6011  eldmeldmressn  6013  resindm  6018  relresdm1  6024  imadisj  6076  imainrect  6172  dmresv  6194  resdmres  6233  resdmss  6236  coeq0  6257  resssxp  6272  snres0  6301  funimacnv  6622  fnresdisj  6660  fnres  6667  fresaunres2  6755  nfvres  6924  ssimaex  6971  fnreseql  7048  respreima  7066  fveqressseq  7080  ffvresb  7127  fsnunfv  7193  funfvima  7237  funiunfv  7253  offres  7996  fnwelem  8146  ressuppss  8204  ressuppssdif  8206  frrlem11  8318  frrlem12  8319  smores  8364  smores3  8365  smores2  8366  tz7.44-2  8419  tz7.44-3  8420  frfnom  8447  sbthlem5  9114  sbthlem7  9116  domss2  9159  imafi  9311  ordtypelem4  9519  wdomima2g  9584  r0weon  10095  imadomg  10617  imadomnum  10618  dmaddpi  10979  dmmulpi  10980  ltweuz  14108  dmhashres  14489  limsupgle  15650  fvsetsid  17352  setsdm  17354  setsfun  17355  setsfun0  17356  setsres  17362  lubdm  18529  glbdm  18542  gsumzaddlem  20141  dprdcntz2  20260  lmres  23624  imacmp  23721  qtoptop2  24024  kqdisj  24057  metreslem  24687  setsmstopn  24803  ismbl  25853  mbfres  25971  dvres3a  26240  cpnres  26263  dvlipcn  26320  dvlip2  26321  c1lip3  26325  dvcnvrelem1  26343  dvcvx  26346  dvlog  26985  ltsres  28025  nolesgn2ores  28035  nogesgn1ores  28037  nodense  28055  nosupres  28070  nosupbnd1lem1  28071  nosupbnd2lem1  28078  nosupbnd2  28079  noinfres  28085  noinfbnd1lem1  28086  noinfbnd2lem1  28093  noetasuplem2  28097  noetainflem2  28101  oniso  28663  bdayn0sf1o  28762  uhgrspansubgrlem  29877  trlsegvdeglem4  30830  hlimcaui  31844  ftc2re  35274  fwfffunres  35765  dfrdg2  36650  bj-fvsnun2  38271  caures  38788  ssbnd  38816  dmcnvepres  39416  dmuncnvepres  39417  dmxrncnvepres2  39459  mapfzcons1  43822  diophrw  43864  eldioph2lem1  43865  eldioph2lem2  43866  tfsconcatrev  44444  limsupresxr  46870  liminfresxr  46871  fourierdlem93  47303  fouriersw  47335  eldmressn  48201  fnresfnco  48205  afvres  48336  afv2res  48403  resinsn  50079  resinsnALT  50080  tposrescnv  50086