Theorem ssdmres 5984

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 3932	. 2 ⊢ (𝐴 ⊆ dom 𝐵 ↔ (𝐴 ∩ dom 𝐵) = 𝐴)
2		dmres 5983	. . 3 ⊢ dom (𝐵 ↾ 𝐴) = (𝐴 ∩ dom 𝐵)
3	2	eqeq1i 2734	. 2 ⊢ (dom (𝐵 ↾ 𝐴) = 𝐴 ↔ (𝐴 ∩ dom 𝐵) = 𝐴)
4	1, 3	bitr4i 278	1 ⊢ (𝐴 ⊆ dom 𝐵 ↔ dom (𝐵 ↾ 𝐴) = 𝐴)

Syntax hints:   ↔ wb 206   = wceq 1540   ∩ cin 3913   ⊆ wss 3914  dom cdm 5638   ↾ cres 5640

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 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-xp 5644  df-dm 5648  df-res 5650

This theorem is referenced by:  dmresi  6023  fnssresb  6640  fores  6782  foimacnv  6817  dffv2  6956  fssrescdmd  7098  sbthlem4  9054  hashres  14403  hashimarn  14405  dvres3  25814  c1liplem1  25901  lhop1lem  25918  lhop  25921  usgrres  29235  vtxdginducedm1lem2  29468  wlkres  29598  trlreslem  29627  cyclnumvtx  29730  hhssabloi  31191  hhssnv  31193  hhshsslem1  31196  fresf1o  32555  fsupprnfi  32615  gsumhashmul  33001  cycpmconjvlem  33098  exidreslem  37871  divrngcl  37951  isdrngo2  37952  n0elqs2  38315  dvbdfbdioolem1  45926  fourierdlem48  46152  fourierdlem49  46153  fourierdlem71  46175  fourierdlem73  46177  fourierdlem94  46198  fourierdlem111  46215  fourierdlem112  46216  fourierdlem113  46217  fouriersw  46229  fouriercn  46230  dmvon  46604  isubgrgrim  47929