Theorem ssdmres 6021

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ⊆ wss 3900   ∩ cin 4092  dom cdm 5658   ↾ cres 5660

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-pr 5398

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109  df-opab 5174  df-xp 5664  df-dm 5668  df-res 5670

This theorem is used by:  dmresi  6062  fnssresb  6691  fores  6836  foimacnv  6872  dffv2  7011  fssrescdmd  7159  sbthlem4  9147  hashres  14624  hashimarn  14626  mgmn0plusgf  18877  dvres3  26288  c1liplem1  26371  lhop1lem  26388  lhop  26391  usgrres  29946  vtxdginducedm1lem2  30178  wlkres  30306  trlreslem  30339  cyclnumvtx  30445  hhssabloi  31921  hhssnv  31923  hhshsslem1  31926  fresf1o  33323  fsupprnfi  33382  gsumhashmul  33727  cycpmconjvlem  33801  fnlfvk30  36068  fnlfvk3n0  36069  nvo3  38230  exidreslem  39077  divrngcl  39157  isdrngo2  39158  n0elqs2  39531  dvbdfbdioolem1  47211  fourierdlem48  47437  fourierdlem49  47438  fourierdlem71  47460  fourierdlem73  47462  fourierdlem94  47483  fourierdlem111  47500  fourierdlem112  47501  fourierdlem113  47502  fouriersw  47514  fouriercn  47515  dmvon  47889  isubgrgrim  49300