Theorem ssdmres 6013

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 3931	. 2 ⊢ (𝐴 ⊆ dom 𝐵 ↔ (𝐴 ∩ dom 𝐵) = 𝐴)
2		dmres 6012	. . 3 ⊢ dom (𝐵 ↾ 𝐴) = (𝐴 ∩ dom 𝐵)
3	2	eqeq1i 2774	. 2 ⊢ (dom (𝐵 ↾ 𝐴) = 𝐴 ↔ (𝐴 ∩ dom 𝐵) = 𝐴)
4	1, 3	bitr4i 281	1 ⊢ (𝐴 ⊆ dom 𝐵 ↔ dom (𝐵 ↾ 𝐴) = 𝐴)

Syntax hints:   ↔ wb 209   = wceq 1567   ∩ cin 3912   ⊆ wss 3913  dom cdm 5662   ↾ cres 5664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-opab 5178  df-xp 5668  df-dm 5672  df-res 5674

This theorem is referenced by:  dmresi  6055  fnssresb  6658  fores  6803  foimacnv  6839  dffv2  6977  fssrescdmd  7123  sbthlem4  9077  hashres  14474  hashimarn  14476  dvres3  26040  c1liplem1  26123  lhop1lem  26140  lhop  26143  usgrres  29598  vtxdginducedm1lem2  29830  wlkres  29958  trlreslem  29987  cyclnumvtx  30089  hhssabloi  31554  hhssnv  31556  hhshsslem1  31559  fresf1o  32916  fsupprnfi  32977  gsumhashmul  33327  cycpmconjvlem  33401  exidreslem  38415  divrngcl  38495  isdrngo2  38496  n0elqs2  38871  dvbdfbdioolem1  46533  fourierdlem48  46759  fourierdlem49  46760  fourierdlem71  46782  fourierdlem73  46784  fourierdlem94  46805  fourierdlem111  46822  fourierdlem112  46823  fourierdlem113  46824  fouriersw  46836  fouriercn  46837  dmvon  47211  isubgrgrim  48582