Theorem ssdmres 5994

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		df-ss 3957	. 2 ⊢ (𝐴 ⊆ dom 𝐵 ↔ (𝐴 ∩ dom 𝐵) = 𝐴)
2		dmres 5993	. . 3 ⊢ dom (𝐵 ↾ 𝐴) = (𝐴 ∩ dom 𝐵)
3	2	eqeq1i 2729	. 2 ⊢ (dom (𝐵 ↾ 𝐴) = 𝐴 ↔ (𝐴 ∩ dom 𝐵) = 𝐴)
4	1, 3	bitr4i 278	1 ⊢ (𝐴 ⊆ dom 𝐵 ↔ dom (𝐵 ↾ 𝐴) = 𝐴)

Syntax hints:   ↔ wb 205   = wceq 1533   ∩ cin 3939   ⊆ wss 3940  dom cdm 5666   ↾ cres 5668

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695  ax-sep 5289  ax-nul 5296  ax-pr 5417

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-sn 4621  df-pr 4623  df-op 4627  df-br 5139  df-opab 5201  df-xp 5672  df-dm 5676  df-res 5678

This theorem is referenced by:  dmresi  6041  fnssresb  6662  fores  6805  foimacnv  6840  dffv2  6976  sbthlem4  9081  hashres  14394  hashimarn  14396  dvres3  25752  c1liplem1  25839  lhop1lem  25856  lhop  25859  usgrres  28989  vtxdginducedm1lem2  29221  wlkres  29351  trlreslem  29380  hhssabloi  30939  hhssnv  30941  hhshsslem1  30944  fresf1o  32279  fsupprnfi  32338  gsumhashmul  32635  cycpmconjvlem  32727  exidreslem  37201  divrngcl  37281  isdrngo2  37282  n0elqs2  37652  dvbdfbdioolem1  45095  fourierdlem48  45321  fourierdlem49  45322  fourierdlem71  45344  fourierdlem73  45346  fourierdlem94  45367  fourierdlem111  45384  fourierdlem112  45385  fourierdlem113  45386  fouriersw  45398  fouriercn  45399  dmvon  45773