Theorem reseq1 5928

Description: Equality theorem for restrictions. (Contributed by NM, 7-Aug-1994.)

Assertion

Ref	Expression
reseq1	⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))

Proof of Theorem reseq1

Step	Hyp	Ref	Expression
1		ineq1 4166	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ (𝐶 × V)) = (𝐵 ∩ (𝐶 × V)))
2		df-res 5635	. 2 ⊢ (𝐴 ↾ 𝐶) = (𝐴 ∩ (𝐶 × V))
3		df-res 5635	. 2 ⊢ (𝐵 ↾ 𝐶) = (𝐵 ∩ (𝐶 × V))
4	1, 2, 3	3eqtr4g 2789	1 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))

Syntax hints:   → wi 4   = wceq 1540  Vcvv 3438   ∩ cin 3904   × cxp 5621   ↾ cres 5625

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-in 3912  df-res 5635

This theorem is referenced by:  reseq1i  5930  reseq1d  5933  imaeq1  6010  fvtresfn  6936  eqfnun  6975  frrlem1  8226  frrlem13  8238  tfrlem12  8318  pmresg  8804  resixpfo  8870  mapunen  9070  fseqenlem1  9937  axdc3lem2  10364  axdc3lem4  10366  hashf1lem1  14380  lo1eq  15493  rlimeq  15494  symgfixfo  19336  lspextmo  20978  evlseu  22006  mdetunilem3  22517  mdetunilem4  22518  mdetunilem9  22523  lmbr  23161  ptuncnv  23710  iscau  25192  plyexmo  26237  relogf1o  26491  nosupprefixmo  27628  noinfprefixmo  27629  nosupcbv  27630  nosupno  27631  nosupdm  27632  nosupfv  27634  nosupres  27635  nosupbnd1lem1  27636  nosupbnd1lem3  27638  nosupbnd1lem5  27640  nosupbnd2  27644  noinfcbv  27645  noinfno  27646  noinfdm  27647  noinffv  27649  noinfres  27650  noinfbnd1lem1  27651  noinfbnd1lem3  27653  noinfbnd1lem5  27655  noinfbnd2  27659  eulerpartlemt  34338  eulerpartlemgv  34340  eulerpartlemn  34348  eulerpart  34349  bnj1385  34798  bnj66  34826  bnj1234  34979  bnj1326  34992  bnj1463  35021  iscvm  35231  mbfresfi  37645  sdclem2  37721  isdivrngo  37929  evlselvlem  42559  evlselv  42560  mzpcompact2lem  42724  diophrw  42732  eldioph2lem1  42733  eldioph2lem2  42734  eldioph3  42739  diophin  42745  diophrex  42748  rexrabdioph  42767  2rexfrabdioph  42769  3rexfrabdioph  42770  4rexfrabdioph  42771  6rexfrabdioph  42772  7rexfrabdioph  42773  eldioph4b  42784  pwssplit4  43062  dvnprodlem1  45928  dvnprodlem3  45930  ismea  46433  isome  46476