Theorem reseq1 5975

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

Syntax hints:   → wi 4   = wceq 1541  Vcvv 3474   ∩ cin 3947   × cxp 5674   ↾ cres 5678

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-in 3955  df-res 5688

This theorem is referenced by:  reseq1i  5977  reseq1d  5980  imaeq1  6054  fvtresfn  7000  eqfnun  7038  frrlem1  8273  frrlem13  8285  wfrlem1OLD  8310  wfrlem3OLDa  8313  wfrlem15OLD  8325  tfrlem12  8391  pmresg  8866  resixpfo  8932  mapunen  9148  fseqenlem1  10021  axdc3lem2  10448  axdc3lem4  10450  axdc  10518  hashf1lem1  14419  hashf1lem1OLD  14420  lo1eq  15516  rlimeq  15517  symgfixfo  19348  lspextmo  20811  evlseu  21865  mdetunilem3  22336  mdetunilem4  22337  mdetunilem9  22342  lmbr  22982  ptuncnv  23531  iscau  25017  plyexmo  26050  relogf1o  26299  nosupprefixmo  27427  noinfprefixmo  27428  nosupcbv  27429  nosupno  27430  nosupdm  27431  nosupfv  27433  nosupres  27434  nosupbnd1lem1  27435  nosupbnd1lem3  27437  nosupbnd1lem5  27439  nosupbnd2  27443  noinfcbv  27444  noinfno  27445  noinfdm  27446  noinffv  27448  noinfres  27449  noinfbnd1lem1  27450  noinfbnd1lem3  27452  noinfbnd1lem5  27454  noinfbnd2  27458  eulerpartlemt  33656  eulerpartlemgv  33658  eulerpartlemn  33666  eulerpart  33667  bnj1385  34129  bnj66  34157  bnj1234  34310  bnj1326  34323  bnj1463  34352  iscvm  34536  mbfresfi  36837  sdclem2  36913  isdivrngo  37121  evlselvlem  41460  evlselv  41461  mzpcompact2lem  41791  diophrw  41799  eldioph2lem1  41800  eldioph2lem2  41801  eldioph3  41806  diophin  41812  diophrex  41815  rexrabdioph  41834  2rexfrabdioph  41836  3rexfrabdioph  41837  4rexfrabdioph  41838  6rexfrabdioph  41839  7rexfrabdioph  41840  eldioph4b  41851  pwssplit4  42133  dvnprodlem1  44961  dvnprodlem3  44963  ismea  45466  isome  45509