Theorem ssdmres 5978

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

Syntax hints:   ↔ wb 206   = wceq 1542   ∩ cin 3888   ⊆ wss 3889  dom cdm 5631   ↾ cres 5633

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 2708  ax-sep 5231  ax-pr 5375

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 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-xp 5637  df-dm 5641  df-res 5643

This theorem is referenced by:  dmresi  6017  fnssresb  6620  fores  6762  foimacnv  6797  dffv2  6935  fssrescdmd  7079  sbthlem4  9028  hashres  14400  hashimarn  14402  dvres3  25880  c1liplem1  25963  lhop1lem  25980  lhop  25983  usgrres  29377  vtxdginducedm1lem2  29609  wlkres  29737  trlreslem  29766  cyclnumvtx  29868  hhssabloi  31333  hhssnv  31335  hhshsslem1  31338  fresf1o  32704  fsupprnfi  32765  gsumhashmul  33128  cycpmconjvlem  33202  exidreslem  38198  divrngcl  38278  isdrngo2  38279  n0elqs2  38654  dvbdfbdioolem1  46356  fourierdlem48  46582  fourierdlem49  46583  fourierdlem71  46605  fourierdlem73  46607  fourierdlem94  46628  fourierdlem111  46645  fourierdlem112  46646  fourierdlem113  46647  fouriersw  46659  fouriercn  46660  dmvon  47034  isubgrgrim  48405