Theorem ssdmres 5972

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

Syntax hints:   ↔ wb 206   = wceq 1542   ∩ cin 3889   ⊆ wss 3890  dom cdm 5624   ↾ cres 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-xp 5630  df-dm 5634  df-res 5636

This theorem is referenced by:  dmresi  6011  fnssresb  6614  fores  6756  foimacnv  6791  dffv2  6929  fssrescdmd  7073  sbthlem4  9021  hashres  14391  hashimarn  14393  dvres3  25890  c1liplem1  25973  lhop1lem  25990  lhop  25993  usgrres  29391  vtxdginducedm1lem2  29624  wlkres  29752  trlreslem  29781  cyclnumvtx  29883  hhssabloi  31348  hhssnv  31350  hhshsslem1  31353  fresf1o  32719  fsupprnfi  32780  gsumhashmul  33143  cycpmconjvlem  33217  exidreslem  38212  divrngcl  38292  isdrngo2  38293  n0elqs2  38668  dvbdfbdioolem1  46374  fourierdlem48  46600  fourierdlem49  46601  fourierdlem71  46623  fourierdlem73  46625  fourierdlem94  46646  fourierdlem111  46663  fourierdlem112  46664  fourierdlem113  46665  fouriersw  46677  fouriercn  46678  dmvon  47052  isubgrgrim  48417