Theorem ssdmres 6031

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∩ cin 3950   ⊆ wss 3951  dom cdm 5685   ↾ cres 5687

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-xp 5691  df-dm 5695  df-res 5697

This theorem is referenced by:  dmresi  6070  fnssresb  6690  fores  6830  foimacnv  6865  dffv2  7004  fssrescdmd  7146  sbthlem4  9126  hashres  14477  hashimarn  14479  dvres3  25948  c1liplem1  26035  lhop1lem  26052  lhop  26055  usgrres  29325  vtxdginducedm1lem2  29558  wlkres  29688  trlreslem  29717  cyclnumvtx  29820  hhssabloi  31281  hhssnv  31283  hhshsslem1  31286  fresf1o  32641  fsupprnfi  32701  gsumhashmul  33064  cycpmconjvlem  33161  exidreslem  37884  divrngcl  37964  isdrngo2  37965  n0elqs2  38328  dvbdfbdioolem1  45943  fourierdlem48  46169  fourierdlem49  46170  fourierdlem71  46192  fourierdlem73  46194  fourierdlem94  46215  fourierdlem111  46232  fourierdlem112  46233  fourierdlem113  46234  fouriersw  46246  fouriercn  46247  dmvon  46621  isubgrgrim  47897