Theorem ssdmres 6032

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 3980	. 2 ⊢ (𝐴 ⊆ dom 𝐵 ↔ (𝐴 ∩ dom 𝐵) = 𝐴)
2		dmres 6031	. . 3 ⊢ dom (𝐵 ↾ 𝐴) = (𝐴 ∩ dom 𝐵)
3	2	eqeq1i 2739	. 2 ⊢ (dom (𝐵 ↾ 𝐴) = 𝐴 ↔ (𝐴 ∩ dom 𝐵) = 𝐴)
4	1, 3	bitr4i 278	1 ⊢ (𝐴 ⊆ dom 𝐵 ↔ dom (𝐵 ↾ 𝐴) = 𝐴)

Syntax hints:   ↔ wb 206   = wceq 1536   ∩ cin 3961   ⊆ wss 3962  dom cdm 5688   ↾ cres 5690

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-xp 5694  df-dm 5698  df-res 5700

This theorem is referenced by:  dmresi  6071  fnssresb  6690  fores  6830  foimacnv  6865  dffv2  7003  fssrescdmd  7145  sbthlem4  9124  hashres  14473  hashimarn  14475  dvres3  25962  c1liplem1  26049  lhop1lem  26066  lhop  26069  usgrres  29339  vtxdginducedm1lem2  29572  wlkres  29702  trlreslem  29731  hhssabloi  31290  hhssnv  31292  hhshsslem1  31295  fresf1o  32647  fsupprnfi  32706  gsumhashmul  33046  cycpmconjvlem  33143  exidreslem  37863  divrngcl  37943  isdrngo2  37944  n0elqs2  38308  dvbdfbdioolem1  45883  fourierdlem48  46109  fourierdlem49  46110  fourierdlem71  46132  fourierdlem73  46134  fourierdlem94  46155  fourierdlem111  46172  fourierdlem112  46173  fourierdlem113  46174  fouriersw  46186  fouriercn  46187  dmvon  46561  isubgrgrim  47834