Theorem reseq1 5974

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

Syntax hints:   → wi 4   = wceq 1570  Vcvv 3455   ∩ cin 3905   × cxp 5661   ↾ cres 5665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-in 3913  df-res 5675

This theorem is referenced by:  reseq1i  5976  reseq1d  5979  imaeq1  6059  fvtresfn  6994  eqfnun  7034  frrlem1  8284  frrlem13  8296  tfrlem12  8377  pmresg  8869  resixpfo  8935  mapunen  9135  fseqenlem1  10009  axdc3lem2  10436  axdc3lem4  10438  hashf1lem1  14494  lo1eq  15621  rlimeq  15622  symgfixfo  19510  lspextmo  21158  evlseu  22215  mdetunilem3  22752  mdetunilem4  22753  mdetunilem9  22758  lmbr  23396  ptuncnv  23945  iscau  25416  plyexmo  26455  relogf1o  26709  nosupprefixmo  27842  noinfprefixmo  27843  nosupcbv  27844  nosupno  27845  nosupdm  27846  nosupfv  27848  nosupres  27849  nosupbnd1lem1  27850  nosupbnd1lem3  27852  nosupbnd1lem5  27854  nosupbnd2  27858  noinfcbv  27859  noinfno  27860  noinfdm  27861  noinffv  27863  noinfres  27864  noinfbnd1lem1  27865  noinfbnd1lem3  27867  noinfbnd1lem5  27869  noinfbnd2  27873  extvfvv  33902  extvfvcl  33904  eulerpartlemt  34739  eulerpartlemgv  34741  eulerpartlemn  34749  eulerpart  34750  bnj1385  35198  bnj66  35226  bnj1234  35379  bnj1326  35392  bnj1463  35421  iscvm  35729  mbfresfi  38295  sdclem2  38371  isdivrngo  38579  evlselvlem  43300  evlselv  43301  mzpcompact2lem  43462  diophrw  43470  eldioph2lem1  43471  eldioph2lem2  43472  eldioph3  43477  diophin  43483  diophrex  43486  rexrabdioph  43501  2rexfrabdioph  43503  3rexfrabdioph  43504  4rexfrabdioph  43505  6rexfrabdioph  43506  7rexfrabdioph  43507  eldioph4b  43518  pwssplit4  43796  dvnprodlem1  46640  dvnprodlem3  46642  ismea  47145  isome  47188