Theorem ssdmres 5420

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 3588	. 2 ⊢ (𝐴 ⊆ dom 𝐵 ↔ (𝐴 ∩ dom 𝐵) = 𝐴)
2		dmres 5419	. . 3 ⊢ dom (𝐵 ↾ 𝐴) = (𝐴 ∩ dom 𝐵)
3	2	eqeq1i 2627	. 2 ⊢ (dom (𝐵 ↾ 𝐴) = 𝐴 ↔ (𝐴 ∩ dom 𝐵) = 𝐴)
4	1, 3	bitr4i 267	1 ⊢ (𝐴 ⊆ dom 𝐵 ↔ dom (𝐵 ↾ 𝐴) = 𝐴)

Syntax hints:   ↔ wb 196   = wceq 1483   ∩ cin 3573   ⊆ wss 3574  dom cdm 5114   ↾ cres 5116

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-xp 5120  df-dm 5124  df-res 5126

This theorem is referenced by:  dmresi  5457  fnssresb  6003  fores  6124  foimacnv  6154  dffv2  6271  sbthlem4  8073  hashres  13225  hashimarn  13227  dvres3  23677  c1liplem1  23759  lhop1lem  23776  lhop  23779  usgrres  26200  vtxdginducedm1lem2  26436  trlreslem  26596  hhssabloi  28119  hhssnv  28121  hhshsslem1  28124  fresf1o  29433  exidreslem  33676  divrngcl  33756  isdrngo2  33757  n0elqs2  34099  dvbdfbdioolem1  40143  fourierdlem48  40371  fourierdlem49  40372  fourierdlem71  40394  fourierdlem73  40396  fourierdlem94  40417  fourierdlem111  40434  fourierdlem112  40435  fourierdlem113  40436  fouriersw  40448  fouriercn  40449  dmvon  40820