Theorem ssdmres 6004

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∩ cin 3898   ⊆ wss 3899  dom cdm 5651   ↾ cres 5653

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5657  df-dm 5661  df-res 5663

This theorem is used by:  dmresi  6044  fnssresb  6659  fores  6804  foimacnv  6840  dffv2  6978  fssrescdmd  7125  sbthlem4  9102  hashres  14576  hashimarn  14578  mgmn0plusgf  18820  dvres3  26226  c1liplem1  26309  lhop1lem  26326  lhop  26329  usgrres  29882  vtxdginducedm1lem2  30114  wlkres  30242  trlreslem  30275  cyclnumvtx  30381  hhssabloi  31857  hhssnv  31859  hhshsslem1  31862  fresf1o  33218  fsupprnfi  33278  gsumhashmul  33621  cycpmconjvlem  33695  exidreslem  38791  divrngcl  38871  isdrngo2  38872  n0elqs2  39245  dvbdfbdioolem1  46907  fourierdlem48  47133  fourierdlem49  47134  fourierdlem71  47156  fourierdlem73  47158  fourierdlem94  47179  fourierdlem111  47196  fourierdlem112  47197  fourierdlem113  47198  fouriersw  47210  fouriercn  47211  dmvon  47585  isubgrgrim  48996