Theorem dmres 6004

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 3468	. . . . 5 ⊢ 𝑥 ∈ V
2	1	eldm2 5886	. . . 4 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵))
3		19.42v 1953	. . . . 5 ⊢ (∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
4		vex 3468	. . . . . . 7 ⊢ 𝑦 ∈ V
5	4	opelresi 5979	. . . . . 6 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
6	5	exbii 1848	. . . . 5 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
7	1	eldm2 5886	. . . . . 6 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
8	7	anbi2i 623	. . . . 5 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
9	3, 6, 8	3bitr4i 303	. . . 4 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴))
10	2, 9	bitr2i 276	. . 3 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ 𝑥 ∈ dom (𝐴 ↾ 𝐵))
11	10	ineqri 4192	. 2 ⊢ (𝐵 ∩ dom 𝐴) = dom (𝐴 ↾ 𝐵)
12	11	eqcomi 2745	1 ⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴)

Syntax hints:   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2109   ∩ cin 3930  ⟨cop 4612  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 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125  df-opab 5187  df-xp 5665  df-dm 5669  df-res 5671

This theorem is referenced by:  ssdmres  6005  dmresexg  6006  dmressnsn  6015  eldmeldmressn  6017  relresdm1  6025  imadisj  6072  imainrect  6175  dmresv  6194  resdmres  6226  resdmss  6229  coeq0  6249  resssxp  6264  snres0  6292  funimacnv  6622  fnresdisj  6663  fnres  6670  fresaunres2  6755  nfvres  6922  ssimaex  6969  fnreseql  7043  respreima  7061  fveqressseq  7074  ffvresb  7120  fsnunfv  7184  funfvima  7227  funiunfv  7245  offres  7987  fnwelem  8135  ressuppss  8187  ressuppssdif  8189  frrlem11  8300  frrlem12  8301  smores  8371  smores3  8372  smores2  8373  tz7.44-2  8426  tz7.44-3  8427  frfnom  8454  sbthlem5  9106  sbthlem7  9108  domss2  9155  imafi  9330  ordtypelem4  9540  wdomima2g  9605  r0weon  10031  imadomg  10553  dmaddpi  10909  dmmulpi  10910  ltweuz  13984  dmhashres  14364  limsupgle  15498  fvsetsid  17192  setsdm  17194  setsfun  17195  setsfun0  17196  setsres  17202  lubdm  18366  glbdm  18379  gsumzaddlem  19907  dprdcntz2  20026  lmres  23243  imacmp  23340  qtoptop2  23642  kqdisj  23675  metreslem  24306  setsmstopn  24422  ismbl  25484  mbfres  25602  dvres3a  25872  cpnres  25896  dvlipcn  25956  dvlip2  25957  c1lip3  25961  dvcnvrelem1  25979  dvcvx  25982  dvlog  26617  sltres  27631  nolesgn2ores  27641  nogesgn1ores  27643  nodense  27661  nosupres  27676  nosupbnd1lem1  27677  nosupbnd2lem1  27684  nosupbnd2  27685  noinfres  27691  noinfbnd1lem1  27692  noinfbnd2lem1  27699  noetasuplem2  27703  noetainflem2  27707  onsiso  28226  bdayn0sf1o  28316  uhgrspansubgrlem  29274  trlsegvdeglem4  30209  hlimcaui  31222  ftc2re  34635  dfrdg2  35818  bj-fvsnun2  37279  caures  37789  ssbnd  37817  mapfzcons1  42707  diophrw  42749  eldioph2lem1  42750  eldioph2lem2  42751  tfsconcatrev  43339  limsupresxr  45762  liminfresxr  45763  fourierdlem93  46195  fouriersw  46227  sssmf  46734  eldmressn  47033  fnresfnco  47037  afvres  47168  afv2res  47235  resinsn  48814  resinsnALT  48815  tposrescnv  48821