Theorem dmres 5983

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 3451	. . . . 5 ⊢ 𝑥 ∈ V
2	1	eldm2 5865	. . . 4 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵))
3		19.42v 1953	. . . . 5 ⊢ (∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴))
4		vex 3451	. . . . . . 7 ⊢ 𝑦 ∈ V
5	4	opelresi 5958	. . . . . 6 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
6	5	exbii 1848	. . . . 5 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ↾ 𝐵) ↔ ∃𝑦(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴))
7	1	eldm2 5865	. . . . . 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 4175	. 2 ⊢ (𝐵 ∩ dom 𝐴) = dom (𝐴 ↾ 𝐵)
12	11	eqcomi 2738	1 ⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴)

Syntax hints:   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2109   ∩ cin 3913  ⟨cop 4595  dom cdm 5638   ↾ cres 5640

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 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

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 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-xp 5644  df-dm 5648  df-res 5650

This theorem is referenced by:  ssdmres  5984  dmresexg  5985  dmressnsn  5994  eldmeldmressn  5996  relresdm1  6004  imadisj  6051  imainrect  6154  dmresv  6173  resdmres  6205  resdmss  6208  coeq0  6228  resssxp  6243  snres0  6271  funimacnv  6597  fnresdisj  6638  fnres  6645  fresaunres2  6732  nfvres  6899  ssimaex  6946  fnreseql  7020  respreima  7038  fveqressseq  7051  ffvresb  7097  fsnunfv  7161  funfvima  7204  funiunfv  7222  offres  7962  fnwelem  8110  ressuppss  8162  ressuppssdif  8164  frrlem11  8275  frrlem12  8276  smores  8321  smores3  8322  smores2  8323  tz7.44-2  8375  tz7.44-3  8376  frfnom  8403  sbthlem5  9055  sbthlem7  9057  domss2  9100  imafi  9264  ordtypelem4  9474  wdomima2g  9539  r0weon  9965  imadomg  10487  dmaddpi  10843  dmmulpi  10844  ltweuz  13926  dmhashres  14306  limsupgle  15443  fvsetsid  17138  setsdm  17140  setsfun  17141  setsfun0  17142  setsres  17148  lubdm  18310  glbdm  18323  gsumzaddlem  19851  dprdcntz2  19970  lmres  23187  imacmp  23284  qtoptop2  23586  kqdisj  23619  metreslem  24250  setsmstopn  24366  ismbl  25427  mbfres  25545  dvres3a  25815  cpnres  25839  dvlipcn  25899  dvlip2  25900  c1lip3  25904  dvcnvrelem1  25922  dvcvx  25925  dvlog  26560  sltres  27574  nolesgn2ores  27584  nogesgn1ores  27586  nodense  27604  nosupres  27619  nosupbnd1lem1  27620  nosupbnd2lem1  27627  nosupbnd2  27628  noinfres  27634  noinfbnd1lem1  27635  noinfbnd2lem1  27642  noetasuplem2  27646  noetainflem2  27650  onsiso  28169  bdayn0sf1o  28259  uhgrspansubgrlem  29217  trlsegvdeglem4  30152  hlimcaui  31165  ftc2re  34589  dfrdg2  35783  bj-fvsnun2  37244  caures  37754  ssbnd  37782  mapfzcons1  42705  diophrw  42747  eldioph2lem1  42748  eldioph2lem2  42749  tfsconcatrev  43337  limsupresxr  45764  liminfresxr  45765  fourierdlem93  46197  fouriersw  46229  sssmf  46736  eldmressn  47035  fnresfnco  47039  afvres  47170  afv2res  47237  resinsn  48857  resinsnALT  48858  tposrescnv  48864