Theorem ssdmres 5964

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∩ cin 3902   ⊆ wss 3903  dom cdm 5619   ↾ cres 5621

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 5235  ax-nul 5245  ax-pr 5371

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155  df-xp 5625  df-dm 5629  df-res 5631

This theorem is referenced by:  dmresi  6003  fnssresb  6604  fores  6746  foimacnv  6781  dffv2  6918  fssrescdmd  7060  sbthlem4  9007  hashres  14345  hashimarn  14347  dvres3  25812  c1liplem1  25899  lhop1lem  25916  lhop  25919  usgrres  29253  vtxdginducedm1lem2  29486  wlkres  29614  trlreslem  29643  cyclnumvtx  29745  hhssabloi  31206  hhssnv  31208  hhshsslem1  31211  fresf1o  32574  fsupprnfi  32634  gsumhashmul  33014  cycpmconjvlem  33083  exidreslem  37857  divrngcl  37937  isdrngo2  37938  n0elqs2  38301  dvbdfbdioolem1  45909  fourierdlem48  46135  fourierdlem49  46136  fourierdlem71  46158  fourierdlem73  46160  fourierdlem94  46181  fourierdlem111  46198  fourierdlem112  46199  fourierdlem113  46200  fouriersw  46212  fouriercn  46213  dmvon  46587  isubgrgrim  47913