Theorem ssdmres 6012

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

Syntax hints:   ↔ wb 209   = wceq 1570   ∩ cin 3904   ⊆ wss 3905  dom cdm 5661   ↾ cres 5663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174  df-xp 5667  df-dm 5671  df-res 5673

This theorem is referenced by:  dmresi  6054  fnssresb  6657  fores  6802  foimacnv  6838  dffv2  6976  fssrescdmd  7122  sbthlem4  9074  hashres  14471  hashimarn  14473  dvres3  26072  c1liplem1  26155  lhop1lem  26172  lhop  26175  usgrres  29658  vtxdginducedm1lem2  29890  wlkres  30018  trlreslem  30047  cyclnumvtx  30149  hhssabloi  31614  hhssnv  31616  hhshsslem1  31619  fresf1o  32976  fsupprnfi  33037  gsumhashmul  33387  cycpmconjvlem  33461  exidreslem  38528  divrngcl  38608  isdrngo2  38609  n0elqs2  38982  dvbdfbdioolem1  46642  fourierdlem48  46868  fourierdlem49  46869  fourierdlem71  46891  fourierdlem73  46893  fourierdlem94  46914  fourierdlem111  46931  fourierdlem112  46932  fourierdlem113  46933  fouriersw  46945  fouriercn  46946  dmvon  47320  isubgrgrim  48694