Theorem dmres 6009

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 3467	. . . . 5 ⊢ 𝑥 ∈ V
2	1	eldm2 5889	. . . 4 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵))
3		19.42v 1980	. . . . 5 ⊢ (∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
4		vex 3467	. . . . . . 7 ⊢ 𝑦 ∈ V
5	4	opelresi 5984	. . . . . 6 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
6	5	exbii 1875	. . . . 5 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
7	1	eldm2 5889	. . . . . 6 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
8	7	anbi2i 634	. . . . 5 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
9	3, 6, 8	3bitr4i 306	. . . 4 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴))
10	2, 9	bitr2i 279	. . 3 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ 𝑥 ∈ dom (𝐴 ↾ 𝐵))
11	10	ineqri 4173	. 2 ⊢ (𝐵 ∩ dom 𝐴) = dom (𝐴 ↾ 𝐵)
12	11	eqcomi 2778	1 ⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴)

Syntax hints:   ∧ wa 400   = wceq 1567  ∃wex 1806   ∈ wcel 2149   ∩ cin 3912  ⟨cop 4597  dom cdm 5659   ↾ cres 5661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5258  ax-pr 5402

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111  df-opab 5175  df-xp 5665  df-dm 5669  df-res 5671

This theorem is referenced by:  ssdmres  6010  dmresexg  6011  dmressnsn  6020  eldmeldmressn  6022  resindm  6027  relresdm1  6033  imadisj  6080  imainrect  6177  dmresv  6197  resdmres  6231  resdmss  6234  coeq0  6255  resssxp  6269  snres0  6297  funimacnv  6615  fnresdisj  6653  fnres  6660  fresaunres2  6748  nfvres  6917  ssimaex  6964  fnreseql  7041  respreima  7059  fveqressseq  7072  ffvresb  7119  fsnunfv  7183  funfvima  7226  funiunfv  7244  offres  7976  fnwelem  8123  ressuppss  8175  ressuppssdif  8177  frrlem11  8289  frrlem12  8290  smores  8335  smores3  8336  smores2  8337  tz7.44-2  8390  tz7.44-3  8391  frfnom  8418  sbthlem5  9075  sbthlem7  9077  domss2  9120  imafi  9271  ordtypelem4  9479  wdomima2g  9544  r0weon  9992  imadomg  10514  dmaddpi  10871  dmmulpi  10872  ltweuz  13993  dmhashres  14373  limsupgle  15524  fvsetsid  17224  setsdm  17226  setsfun  17227  setsfun0  17228  setsres  17234  lubdm  18401  glbdm  18414  gsumzaddlem  19987  dprdcntz2  20106  lmres  23422  imacmp  23519  qtoptop2  23821  kqdisj  23854  metreslem  24484  setsmstopn  24600  ismbl  25650  mbfres  25768  dvres3a  26038  cpnres  26061  dvlipcn  26118  dvlip2  26119  c1lip3  26123  dvcnvrelem1  26141  dvcvx  26144  dvlog  26778  ltsres  27788  nolesgn2ores  27798  nogesgn1ores  27800  nodense  27818  nosupres  27833  nosupbnd1lem1  27834  nosupbnd2lem1  27841  nosupbnd2  27842  noinfres  27848  noinfbnd1lem1  27849  noinfbnd2lem1  27856  noetasuplem2  27860  noetainflem2  27864  oniso  28426  bdayn0sf1o  28525  uhgrspansubgrlem  29577  trlsegvdeglem4  30511  hlimcaui  31525  ftc2re  34926  dfrdg2  36180  bj-fvsnun2  37783  caures  38294  ssbnd  38322  dmcnvepres  38924  dmuncnvepres  38925  dmxrncnvepres2  38967  mapfzcons1  43335  diophrw  43377  eldioph2lem1  43378  eldioph2lem2  43379  tfsconcatrev  43962  limsupresxr  46367  liminfresxr  46368  fourierdlem93  46800  fouriersw  46832  eldmressn  47658  fnresfnco  47662  afvres  47793  afv2res  47860  resinsn  49530  resinsnALT  49531  tposrescnv  49537