Theorem ssdmres 5969

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

Syntax hints:   ↔ wb 206   = wceq 1541   ∩ cin 3897   ⊆ wss 3898  dom cdm 5621   ↾ cres 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096  df-opab 5158  df-xp 5627  df-dm 5631  df-res 5633

This theorem is referenced by:  dmresi  6008  fnssresb  6611  fores  6753  foimacnv  6788  dffv2  6926  fssrescdmd  7068  sbthlem4  9014  hashres  14352  hashimarn  14354  dvres3  25861  c1liplem1  25948  lhop1lem  25965  lhop  25968  usgrres  29307  vtxdginducedm1lem2  29540  wlkres  29668  trlreslem  29697  cyclnumvtx  29799  hhssabloi  31263  hhssnv  31265  hhshsslem1  31268  fresf1o  32635  fsupprnfi  32697  gsumhashmul  33078  cycpmconjvlem  33151  exidreslem  37990  divrngcl  38070  isdrngo2  38071  n0elqs2  38438  dvbdfbdioolem1  46088  fourierdlem48  46314  fourierdlem49  46315  fourierdlem71  46337  fourierdlem73  46339  fourierdlem94  46360  fourierdlem111  46377  fourierdlem112  46378  fourierdlem113  46379  fouriersw  46391  fouriercn  46392  dmvon  46766  isubgrgrim  48091