Theorem ssdmres 5973

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 3929	. 2 ⊢ (𝐴 ⊆ dom 𝐵 ↔ (𝐴 ∩ dom 𝐵) = 𝐴)
2		dmres 5972	. . 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 3910   ⊆ wss 3911  dom cdm 5631   ↾ cres 5633

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 5246  ax-nul 5256  ax-pr 5382

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-xp 5637  df-dm 5641  df-res 5643

This theorem is referenced by:  dmresi  6012  fnssresb  6622  fores  6764  foimacnv  6799  dffv2  6938  fssrescdmd  7080  sbthlem4  9031  hashres  14379  hashimarn  14381  dvres3  25790  c1liplem1  25877  lhop1lem  25894  lhop  25897  usgrres  29211  vtxdginducedm1lem2  29444  wlkres  29572  trlreslem  29601  cyclnumvtx  29703  hhssabloi  31164  hhssnv  31166  hhshsslem1  31169  fresf1o  32528  fsupprnfi  32588  gsumhashmul  32974  cycpmconjvlem  33071  exidreslem  37844  divrngcl  37924  isdrngo2  37925  n0elqs2  38288  dvbdfbdioolem1  45899  fourierdlem48  46125  fourierdlem49  46126  fourierdlem71  46148  fourierdlem73  46150  fourierdlem94  46171  fourierdlem111  46188  fourierdlem112  46189  fourierdlem113  46190  fouriersw  46202  fouriercn  46203  dmvon  46577  isubgrgrim  47902