Theorem ssdmres 5987

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∩ cin 3916   ⊆ wss 3917  dom cdm 5641   ↾ cres 5643

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-xp 5647  df-dm 5651  df-res 5653

This theorem is referenced by:  dmresi  6026  fnssresb  6643  fores  6785  foimacnv  6820  dffv2  6959  fssrescdmd  7101  sbthlem4  9060  hashres  14410  hashimarn  14412  dvres3  25821  c1liplem1  25908  lhop1lem  25925  lhop  25928  usgrres  29242  vtxdginducedm1lem2  29475  wlkres  29605  trlreslem  29634  cyclnumvtx  29737  hhssabloi  31198  hhssnv  31200  hhshsslem1  31203  fresf1o  32562  fsupprnfi  32622  gsumhashmul  33008  cycpmconjvlem  33105  exidreslem  37878  divrngcl  37958  isdrngo2  37959  n0elqs2  38322  dvbdfbdioolem1  45933  fourierdlem48  46159  fourierdlem49  46160  fourierdlem71  46182  fourierdlem73  46184  fourierdlem94  46205  fourierdlem111  46222  fourierdlem112  46223  fourierdlem113  46224  fouriersw  46236  fouriercn  46237  dmvon  46611  isubgrgrim  47933