Theorem reseq1 5926

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

Syntax hints:   → wi 4   = wceq 1541  Vcvv 3437   ∩ cin 3897   × cxp 5617   ↾ cres 5621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-in 3905  df-res 5631

This theorem is referenced by:  reseq1i  5928  reseq1d  5931  imaeq1  6008  fvtresfn  6937  eqfnun  6976  frrlem1  8222  frrlem13  8234  tfrlem12  8314  pmresg  8800  resixpfo  8866  mapunen  9066  fseqenlem1  9922  axdc3lem2  10349  axdc3lem4  10351  hashf1lem1  14364  lo1eq  15477  rlimeq  15478  symgfixfo  19353  lspextmo  20992  evlseu  22019  mdetunilem3  22530  mdetunilem4  22531  mdetunilem9  22536  lmbr  23174  ptuncnv  23723  iscau  25204  plyexmo  26249  relogf1o  26503  nosupprefixmo  27640  noinfprefixmo  27641  nosupcbv  27642  nosupno  27643  nosupdm  27644  nosupfv  27646  nosupres  27647  nosupbnd1lem1  27648  nosupbnd1lem3  27650  nosupbnd1lem5  27652  nosupbnd2  27656  noinfcbv  27657  noinfno  27658  noinfdm  27659  noinffv  27661  noinfres  27662  noinfbnd1lem1  27663  noinfbnd1lem3  27665  noinfbnd1lem5  27667  noinfbnd2  27671  extvfvv  33585  extvfvcl  33587  eulerpartlemt  34405  eulerpartlemgv  34407  eulerpartlemn  34415  eulerpart  34416  bnj1385  34865  bnj66  34893  bnj1234  35046  bnj1326  35059  bnj1463  35088  iscvm  35324  mbfresfi  37726  sdclem2  37802  isdivrngo  38010  evlselvlem  42704  evlselv  42705  mzpcompact2lem  42868  diophrw  42876  eldioph2lem1  42877  eldioph2lem2  42878  eldioph3  42883  diophin  42889  diophrex  42892  rexrabdioph  42911  2rexfrabdioph  42913  3rexfrabdioph  42914  4rexfrabdioph  42915  6rexfrabdioph  42916  7rexfrabdioph  42917  eldioph4b  42928  pwssplit4  43206  dvnprodlem1  46068  dvnprodlem3  46070  ismea  46573  isome  46616