Theorem dmres 5994

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 3457	. . . . 5 ⊢ 𝑥 ∈ V
2	1	eldm2 5873	. . . 4 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵))
3		19.42v 1972	. . . . 5 ⊢ (∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
4		vex 3457	. . . . . . 7 ⊢ 𝑦 ∈ V
5	4	opelresi 5969	. . . . . 6 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
6	5	exbii 1867	. . . . 5 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
7	1	eldm2 5873	. . . . . 6 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
8	7	anbi2i 632	. . . . 5 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
9	3, 6, 8	3bitr4i 305	. . . 4 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴))
10	2, 9	bitr2i 278	. . 3 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ dom 𝐴) ↔ 𝑥 ∈ dom (𝐴 ↾ 𝐵))
11	10	ineqri 4162	. 2 ⊢ (𝐵 ∩ dom 𝐴) = dom (𝐴 ↾ 𝐵)
12	11	eqcomi 2770	1 ⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴)

Syntax hints:   ∧ wa 399   = wceq 1559  ∃wex 1798   ∈ wcel 2141   ∩ cin 3901  ⟨cop 4585  dom cdm 5643   ↾ cres 5645

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5243  ax-pr 5387

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098  df-opab 5160  df-xp 5649  df-dm 5653  df-res 5655

This theorem is referenced by:  ssdmres  5995  dmresexg  5996  dmressnsn  6005  eldmeldmressn  6007  resindm  6012  relresdm1  6018  imadisj  6065  imainrect  6162  dmresv  6182  resdmres  6214  resdmss  6217  coeq0  6238  resssxp  6252  snres0  6280  funimacnv  6597  fnresdisj  6636  fnres  6643  fresaunres2  6731  nfvres  6900  ssimaex  6947  fnreseql  7024  respreima  7042  fveqressseq  7055  ffvresb  7102  fsnunfv  7166  funfvima  7209  funiunfv  7227  offres  7959  fnwelem  8105  ressuppss  8157  ressuppssdif  8159  frrlem11  8271  frrlem12  8272  smores  8317  smores3  8318  smores2  8319  tz7.44-2  8372  tz7.44-3  8373  frfnom  8400  sbthlem5  9057  sbthlem7  9059  domss2  9102  imafi  9253  ordtypelem4  9463  wdomima2g  9528  r0weon  9962  imadomg  10485  dmaddpi  10842  dmmulpi  10843  ltweuz  13968  dmhashres  14348  limsupgle  15495  fvsetsid  17195  setsdm  17197  setsfun  17198  setsfun0  17199  setsres  17205  lubdm  18372  glbdm  18385  gsumzaddlem  19952  dprdcntz2  20071  lmres  23348  imacmp  23445  qtoptop2  23747  kqdisj  23780  metreslem  24410  setsmstopn  24526  ismbl  25576  mbfres  25694  dvres3a  25964  cpnres  25987  dvlipcn  26044  dvlip2  26045  c1lip3  26049  dvcnvrelem1  26067  dvcvx  26070  dvlog  26704  ltsres  27714  nolesgn2ores  27724  nogesgn1ores  27726  nodense  27744  nosupres  27759  nosupbnd1lem1  27760  nosupbnd2lem1  27767  nosupbnd2  27768  noinfres  27774  noinfbnd1lem1  27775  noinfbnd2lem1  27782  noetasuplem2  27786  noetainflem2  27790  oniso  28352  bdayn0sf1o  28451  uhgrspansubgrlem  29448  trlsegvdeglem4  30382  hlimcaui  31396  ftc2re  34853  dfrdg2  36104  bj-fvsnun2  37709  caures  38220  ssbnd  38248  dmcnvepres  38850  dmuncnvepres  38851  dmxrncnvepres2  38893  mapfzcons1  43259  diophrw  43301  eldioph2lem1  43302  eldioph2lem2  43303  tfsconcatrev  43886  limsupresxr  46301  liminfresxr  46302  fourierdlem93  46734  fouriersw  46766  eldmressn  47592  fnresfnco  47596  afvres  47727  afv2res  47794  resinsn  49454  resinsnALT  49455  tposrescnv  49461