Theorem ssdmres 5995

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 3920	. 2 ⊢ (𝐴 ⊆ dom 𝐵 ↔ (𝐴 ∩ dom 𝐵) = 𝐴)
2		dmres 5994	. . 3 ⊢ dom (𝐵 ↾ 𝐴) = (𝐴 ∩ dom 𝐵)
3	2	eqeq1i 2766	. 2 ⊢ (dom (𝐵 ↾ 𝐴) = 𝐴 ↔ (𝐴 ∩ dom 𝐵) = 𝐴)
4	1, 3	bitr4i 280	1 ⊢ (𝐴 ⊆ dom 𝐵 ↔ dom (𝐵 ↾ 𝐴) = 𝐴)

Syntax hints:   ↔ wb 208   = wceq 1559   ∩ cin 3901   ⊆ wss 3902  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:  dmresi  6037  fnssresb  6638  fores  6783  foimacnv  6819  dffv2  6957  fssrescdmd  7103  sbthlem4  9056  hashres  14445  hashimarn  14447  dvres3  25963  c1liplem1  26046  lhop1lem  26063  lhop  26066  usgrres  29466  vtxdginducedm1lem2  29698  wlkres  29826  trlreslem  29855  cyclnumvtx  29957  hhssabloi  31422  hhssnv  31424  hhshsslem1  31427  fresf1o  32794  fsupprnfi  32855  gsumhashmul  33208  cycpmconjvlem  33282  exidreslem  38337  divrngcl  38417  isdrngo2  38418  n0elqs2  38793  dvbdfbdioolem1  46463  fourierdlem48  46689  fourierdlem49  46690  fourierdlem71  46712  fourierdlem73  46714  fourierdlem94  46735  fourierdlem111  46752  fourierdlem112  46753  fourierdlem113  46754  fouriersw  46766  fouriercn  46767  dmvon  47141  isubgrgrim  48512