Theorem ssdmres 6042

Description: A domain restricted to a subclass equals the subclass. (Contributed by NM, 2-Mar-1997.)

Assertion

Ref	Expression
ssdmres	⊢ (𝐴 ⊆ dom 𝐵 ↔ dom (𝐵 ↾ 𝐴) = 𝐴)

Proof of Theorem ssdmres

Step	Hyp	Ref	Expression
1		dfss2 3994	. 2 ⊢ (𝐴 ⊆ dom 𝐵 ↔ (𝐴 ∩ dom 𝐵) = 𝐴)
2		dmres 6041	. . 3 ⊢ dom (𝐵 ↾ 𝐴) = (𝐴 ∩ dom 𝐵)
3	2	eqeq1i 2745	. 2 ⊢ (dom (𝐵 ↾ 𝐴) = 𝐴 ↔ (𝐴 ∩ dom 𝐵) = 𝐴)
4	1, 3	bitr4i 278	1 ⊢ (𝐴 ⊆ dom 𝐵 ↔ dom (𝐵 ↾ 𝐴) = 𝐴)

Syntax hints:   ↔ wb 206   = wceq 1537   ∩ cin 3975   ⊆ wss 3976  dom cdm 5700   ↾ cres 5702

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-xp 5706  df-dm 5710  df-res 5712

This theorem is referenced by:  dmresi  6081  fnssresb  6702  fores  6844  foimacnv  6879  dffv2  7017  fssrescdmd  7160  sbthlem4  9152  hashres  14487  hashimarn  14489  dvres3  25968  c1liplem1  26055  lhop1lem  26072  lhop  26075  usgrres  29343  vtxdginducedm1lem2  29576  wlkres  29706  trlreslem  29735  hhssabloi  31294  hhssnv  31296  hhshsslem1  31299  fresf1o  32650  fsupprnfi  32704  gsumhashmul  33040  cycpmconjvlem  33134  exidreslem  37837  divrngcl  37917  isdrngo2  37918  n0elqs2  38283  dvbdfbdioolem1  45849  fourierdlem48  46075  fourierdlem49  46076  fourierdlem71  46098  fourierdlem73  46100  fourierdlem94  46121  fourierdlem111  46138  fourierdlem112  46139  fourierdlem113  46140  fouriersw  46152  fouriercn  46153  dmvon  46527  isubgrgrim  47781