Theorem dmres 6020

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 3465	. . . . 5 ⊢ 𝑥 ∈ V
2	1	eldm2 5907	. . . 4 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵))
3		19.42v 1949	. . . . 5 ⊢ (∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
4		vex 3465	. . . . . . 7 ⊢ 𝑦 ∈ V
5	4	opelresi 5996	. . . . . 6 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
6	5	exbii 1842	. . . . 5 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
7	1	eldm2 5907	. . . . . 6 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
8	7	anbi2i 621	. . . . 5 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
9	3, 6, 8	3bitr4i 302	. . . 4 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴))
10	2, 9	bitr2i 275	. . 3 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ 𝑥 ∈ dom (𝐴 ↾ 𝐵))
11	10	ineqri 4204	. 2 ⊢ (𝐵 ∩ dom 𝐴) = dom (𝐴 ↾ 𝐵)
12	11	eqcomi 2734	1 ⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴)

Syntax hints:   ∧ wa 394   = wceq 1533  ∃wex 1773   ∈ wcel 2098   ∩ cin 3945  ⟨cop 4638  dom cdm 5681   ↾ cres 5683

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-sep 5303  ax-nul 5310  ax-pr 5432

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4325  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-br 5153  df-opab 5215  df-xp 5687  df-dm 5691  df-res 5693

This theorem is referenced by:  ssdmres  6021  dmresexg  6022  dmressnsn  6031  eldmeldmressn  6033  relresdm1  6041  imadisj  6088  imainrect  6191  dmresv  6210  resdmres  6242  resdmss  6245  coeq0  6265  resssxp  6280  snres0  6308  funimacnv  6639  fnresdisj  6680  fnres  6687  fresaunres2  6773  nfvres  6941  ssimaex  6986  fnreseql  7060  respreima  7078  fveqressseq  7092  ffvresb  7138  fsnunfv  7200  funfvima  7246  funiunfv  7262  offres  7996  fnwelem  8144  ressuppss  8196  ressuppssdif  8198  frrlem11  8310  frrlem12  8311  smores  8381  smores3  8382  smores2  8383  tz7.44-2  8436  tz7.44-3  8437  frfnom  8464  sbthlem5  9124  sbthlem7  9126  domss2  9173  imafiALT  9385  ordtypelem4  9560  wdomima2g  9625  r0weon  10051  imadomg  10573  dmaddpi  10929  dmmulpi  10930  ltweuz  13976  dmhashres  14353  limsupgle  15474  fvsetsid  17165  setsdm  17167  setsfun  17168  setsfun0  17169  setsres  17175  lubdm  18371  glbdm  18384  gsumzaddlem  19914  dprdcntz2  20033  lmres  23287  imacmp  23384  qtoptop2  23686  kqdisj  23719  metreslem  24351  setsmstopn  24469  ismbl  25538  mbfres  25656  dvres3a  25926  cpnres  25950  dvlipcn  26010  dvlip2  26011  c1lip3  26015  dvcnvrelem1  26033  dvcvx  26036  dvlog  26670  sltres  27684  nolesgn2ores  27694  nogesgn1ores  27696  nodense  27714  nosupres  27729  nosupbnd1lem1  27730  nosupbnd2lem1  27737  nosupbnd2  27738  noinfres  27744  noinfbnd1lem1  27745  noinfbnd2lem1  27752  noetasuplem2  27756  noetainflem2  27760  uhgrspansubgrlem  29218  trlsegvdeglem4  30148  hlimcaui  31161  ftc2re  34400  dfrdg2  35567  bj-fvsnun2  36911  caures  37409  ssbnd  37437  mapfzcons1  42311  diophrw  42353  eldioph2lem1  42354  eldioph2lem2  42355  tfsconcatrev  42951  limsupresxr  45324  liminfresxr  45325  fourierdlem93  45757  fouriersw  45789  sssmf  46296  eldmressn  46589  fnresfnco  46593  afvres  46722  afv2res  46789