Theorem ssdmres 5965

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 3901	. 2 ⊢ (𝐴 ⊆ dom 𝐵 ↔ (𝐴 ∩ dom 𝐵) = 𝐴)
2		dmres 5964	. . 3 ⊢ dom (𝐵 ↾ 𝐴) = (𝐴 ∩ dom 𝐵)
3	2	eqeq1i 2744	. 2 ⊢ (dom (𝐵 ↾ 𝐴) = 𝐴 ↔ (𝐴 ∩ dom 𝐵) = 𝐴)
4	1, 3	bitr4i 279	1 ⊢ (𝐴 ⊆ dom 𝐵 ↔ dom (𝐵 ↾ 𝐴) = 𝐴)

Syntax hints:   ↔ wb 207   = wceq 1547   ∩ cin 3882   ⊆ wss 3883  dom cdm 5618   ↾ cres 5620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-xp 5624  df-dm 5628  df-res 5630

This theorem is referenced by:  dmresi  6004  fnssresb  6607  fores  6749  foimacnv  6784  dffv2  6922  fssrescdmd  7068  sbthlem4  9018  hashres  14391  hashimarn  14393  dvres3  25898  c1liplem1  25981  lhop1lem  25998  lhop  26001  usgrres  29395  vtxdginducedm1lem2  29627  wlkres  29755  trlreslem  29784  cyclnumvtx  29886  hhssabloi  31351  hhssnv  31353  hhshsslem1  31356  fresf1o  32723  fsupprnfi  32784  gsumhashmul  33148  cycpmconjvlem  33222  exidreslem  38244  divrngcl  38324  isdrngo2  38325  n0elqs2  38700  dvbdfbdioolem1  46371  fourierdlem48  46597  fourierdlem49  46598  fourierdlem71  46620  fourierdlem73  46622  fourierdlem94  46643  fourierdlem111  46660  fourierdlem112  46661  fourierdlem113  46662  fouriersw  46674  fouriercn  46675  dmvon  47049  isubgrgrim  48420