Theorem ssdmres 6006

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 6005	. . 3 ⊢ dom (𝐵 ↾ 𝐴) = (𝐴 ∩ dom 𝐵)
3	2	eqeq1i 2765	. 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 5655   ↾ cres 5657

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 2732  ax-sep 5251  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 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  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 5661  df-dm 5665  df-res 5667

This theorem is used by:  dmresi  6048  fnssresb  6654  fores  6799  foimacnv  6835  dffv2  6973  fssrescdmd  7120  sbthlem4  9088  hashres  14503  hashimarn  14505  mgmn0plusgf  18741  dvres3  26140  c1liplem1  26223  lhop1lem  26240  lhop  26243  usgrres  29768  vtxdginducedm1lem2  30000  wlkres  30128  trlreslem  30161  cyclnumvtx  30267  hhssabloi  31743  hhssnv  31745  hhshsslem1  31748  fresf1o  33104  fsupprnfi  33164  gsumhashmul  33507  cycpmconjvlem  33581  exidreslem  38627  divrngcl  38707  isdrngo2  38708  n0elqs2  39081  dvbdfbdioolem1  46756  fourierdlem48  46982  fourierdlem49  46983  fourierdlem71  47005  fourierdlem73  47007  fourierdlem94  47028  fourierdlem111  47045  fourierdlem112  47046  fourierdlem113  47047  fouriersw  47059  fouriercn  47060  dmvon  47434  isubgrgrim  48845