Theorem dmres 5971

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 3444	. . . . 5 ⊢ 𝑥 ∈ V
2	1	eldm2 5850	. . . 4 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵))
3		19.42v 1954	. . . . 5 ⊢ (∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
4		vex 3444	. . . . . . 7 ⊢ 𝑦 ∈ V
5	4	opelresi 5946	. . . . . 6 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
6	5	exbii 1849	. . . . 5 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
7	1	eldm2 5850	. . . . . 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 4164	. 2 ⊢ (𝐵 ∩ dom 𝐴) = dom (𝐴 ↾ 𝐵)
12	11	eqcomi 2745	1 ⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴)

Syntax hints:   ∧ wa 395   = wceq 1541  ∃wex 1780   ∈ wcel 2113   ∩ cin 3900  ⟨cop 4586  dom cdm 5624   ↾ cres 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-xp 5630  df-dm 5634  df-res 5636

This theorem is referenced by:  ssdmres  5972  dmresexg  5973  dmressnsn  5982  eldmeldmressn  5984  relresdm1  5992  imadisj  6039  imainrect  6139  dmresv  6158  resdmres  6190  resdmss  6193  coeq0  6214  resssxp  6228  snres0  6256  funimacnv  6573  fnresdisj  6612  fnres  6619  fresaunres2  6706  nfvres  6872  ssimaex  6919  fnreseql  6993  respreima  7011  fveqressseq  7024  ffvresb  7070  fsnunfv  7133  funfvima  7176  funiunfv  7194  offres  7927  fnwelem  8073  ressuppss  8125  ressuppssdif  8127  frrlem11  8238  frrlem12  8239  smores  8284  smores3  8285  smores2  8286  tz7.44-2  8338  tz7.44-3  8339  frfnom  8366  sbthlem5  9019  sbthlem7  9021  domss2  9064  imafi  9215  ordtypelem4  9426  wdomima2g  9491  r0weon  9922  imadomg  10444  dmaddpi  10801  dmmulpi  10802  ltweuz  13884  dmhashres  14264  limsupgle  15400  fvsetsid  17095  setsdm  17097  setsfun  17098  setsfun0  17099  setsres  17105  lubdm  18272  glbdm  18285  gsumzaddlem  19850  dprdcntz2  19969  lmres  23244  imacmp  23341  qtoptop2  23643  kqdisj  23676  metreslem  24306  setsmstopn  24422  ismbl  25483  mbfres  25601  dvres3a  25871  cpnres  25895  dvlipcn  25955  dvlip2  25956  c1lip3  25960  dvcnvrelem1  25978  dvcvx  25981  dvlog  26616  ltsres  27630  nolesgn2ores  27640  nogesgn1ores  27642  nodense  27660  nosupres  27675  nosupbnd1lem1  27676  nosupbnd2lem1  27683  nosupbnd2  27684  noinfres  27690  noinfbnd1lem1  27691  noinfbnd2lem1  27698  noetasuplem2  27702  noetainflem2  27706  oniso  28267  bdayn0sf1o  28366  uhgrspansubgrlem  29363  trlsegvdeglem4  30298  hlimcaui  31311  ftc2re  34755  dfrdg2  35987  bj-fvsnun2  37461  caures  37961  ssbnd  37989  dmcnvepres  38575  dmuncnvepres  38576  dmxrncnvepres2  38618  mapfzcons1  42959  diophrw  43001  eldioph2lem1  43002  eldioph2lem2  43003  tfsconcatrev  43590  limsupresxr  46010  liminfresxr  46011  fourierdlem93  46443  fouriersw  46475  sssmf  46982  eldmressn  47283  fnresfnco  47287  afvres  47418  afv2res  47485  resinsn  49117  resinsnALT  49118  tposrescnv  49124