Theorem ssdmres 5869

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 3945	. 2 ⊢ (𝐴 ⊆ dom 𝐵 ↔ (𝐴 ∩ dom 𝐵) = 𝐴)
2		dmres 5868	. . 3 ⊢ dom (𝐵 ↾ 𝐴) = (𝐴 ∩ dom 𝐵)
3	2	eqeq1i 2825	. 2 ⊢ (dom (𝐵 ↾ 𝐴) = 𝐴 ↔ (𝐴 ∩ dom 𝐵) = 𝐴)
4	1, 3	bitr4i 280	1 ⊢ (𝐴 ⊆ dom 𝐵 ↔ dom (𝐵 ↾ 𝐴) = 𝐴)

Syntax hints:   ↔ wb 208   = wceq 1536   ∩ cin 3928   ⊆ wss 3929  dom cdm 5548   ↾ cres 5550

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2792  ax-sep 5196  ax-nul 5203  ax-pr 5323

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2799  df-cleq 2813  df-clel 2892  df-nfc 2962  df-ral 3142  df-rex 3143  df-rab 3146  df-v 3493  df-dif 3932  df-un 3934  df-in 3936  df-ss 3945  df-nul 4285  df-if 4461  df-sn 4561  df-pr 4563  df-op 4567  df-br 5060  df-opab 5122  df-xp 5554  df-dm 5558  df-res 5560

This theorem is referenced by:  dmresi  5914  fnssresb  6462  fores  6593  foimacnv  6625  dffv2  6749  sbthlem4  8623  hashres  13796  hashimarn  13798  dvres3  24508  c1liplem1  24590  lhop1lem  24607  lhop  24610  usgrres  27088  vtxdginducedm1lem2  27320  wlkres  27450  trlreslem  27479  hhssabloi  29037  hhssnv  29039  hhshsslem1  29042  fresf1o  30376  cycpmconjvlem  30804  exidreslem  35188  divrngcl  35268  isdrngo2  35269  n0elqs2  35617  dvbdfbdioolem1  42287  fourierdlem48  42513  fourierdlem49  42514  fourierdlem71  42536  fourierdlem73  42538  fourierdlem94  42559  fourierdlem111  42576  fourierdlem112  42577  fourierdlem113  42578  fouriersw  42590  fouriercn  42591  dmvon  42962