Theorem reseq1 5973

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 4201	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ (𝐶 × V)) = (𝐵 ∩ (𝐶 × V)))
2		df-res 5684	. 2 ⊢ (𝐴 ↾ 𝐶) = (𝐴 ∩ (𝐶 × V))
3		df-res 5684	. 2 ⊢ (𝐵 ↾ 𝐶) = (𝐵 ∩ (𝐶 × V))
4	1, 2, 3	3eqtr4g 2793	1 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))

Syntax hints:   → wi 4   = wceq 1534  Vcvv 3470   ∩ cin 3944   × cxp 5670   ↾ cres 5674

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3429  df-in 3952  df-res 5684

This theorem is referenced by:  reseq1i  5975  reseq1d  5978  imaeq1  6052  fvtresfn  7001  eqfnun  7040  frrlem1  8285  frrlem13  8297  wfrlem1OLD  8322  wfrlem3OLDa  8325  wfrlem15OLD  8337  tfrlem12  8403  pmresg  8882  resixpfo  8948  mapunen  9164  fseqenlem1  10041  axdc3lem2  10468  axdc3lem4  10470  axdc  10538  hashf1lem1  14441  hashf1lem1OLD  14442  lo1eq  15538  rlimeq  15539  symgfixfo  19387  lspextmo  20934  evlseu  22022  mdetunilem3  22509  mdetunilem4  22510  mdetunilem9  22515  lmbr  23155  ptuncnv  23704  iscau  25197  plyexmo  26241  relogf1o  26493  nosupprefixmo  27626  noinfprefixmo  27627  nosupcbv  27628  nosupno  27629  nosupdm  27630  nosupfv  27632  nosupres  27633  nosupbnd1lem1  27634  nosupbnd1lem3  27636  nosupbnd1lem5  27638  nosupbnd2  27642  noinfcbv  27643  noinfno  27644  noinfdm  27645  noinffv  27647  noinfres  27648  noinfbnd1lem1  27649  noinfbnd1lem3  27651  noinfbnd1lem5  27653  noinfbnd2  27657  eulerpartlemt  33985  eulerpartlemgv  33987  eulerpartlemn  33995  eulerpart  33996  bnj1385  34457  bnj66  34485  bnj1234  34638  bnj1326  34651  bnj1463  34680  iscvm  34863  mbfresfi  37133  sdclem2  37209  isdivrngo  37417  evlselvlem  41813  evlselv  41814  mzpcompact2lem  42165  diophrw  42173  eldioph2lem1  42174  eldioph2lem2  42175  eldioph3  42180  diophin  42186  diophrex  42189  rexrabdioph  42208  2rexfrabdioph  42210  3rexfrabdioph  42211  4rexfrabdioph  42212  6rexfrabdioph  42213  7rexfrabdioph  42214  eldioph4b  42225  pwssplit4  42507  dvnprodlem1  45328  dvnprodlem3  45330  ismea  45833  isome  45876