Theorem reseq1 5947

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

Syntax hints:   → wi 4   = wceq 1540  Vcvv 3450   ∩ cin 3916   × cxp 5639   ↾ cres 5643

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-in 3924  df-res 5653

This theorem is referenced by:  reseq1i  5949  reseq1d  5952  imaeq1  6029  fvtresfn  6973  eqfnun  7012  frrlem1  8268  frrlem13  8280  tfrlem12  8360  pmresg  8846  resixpfo  8912  mapunen  9116  fseqenlem1  9984  axdc3lem2  10411  axdc3lem4  10413  hashf1lem1  14427  lo1eq  15541  rlimeq  15542  symgfixfo  19376  lspextmo  20970  evlseu  21997  mdetunilem3  22508  mdetunilem4  22509  mdetunilem9  22514  lmbr  23152  ptuncnv  23701  iscau  25183  plyexmo  26228  relogf1o  26482  nosupprefixmo  27619  noinfprefixmo  27620  nosupcbv  27621  nosupno  27622  nosupdm  27623  nosupfv  27625  nosupres  27626  nosupbnd1lem1  27627  nosupbnd1lem3  27629  nosupbnd1lem5  27631  nosupbnd2  27635  noinfcbv  27636  noinfno  27637  noinfdm  27638  noinffv  27640  noinfres  27641  noinfbnd1lem1  27642  noinfbnd1lem3  27644  noinfbnd1lem5  27646  noinfbnd2  27650  eulerpartlemt  34369  eulerpartlemgv  34371  eulerpartlemn  34379  eulerpart  34380  bnj1385  34829  bnj66  34857  bnj1234  35010  bnj1326  35023  bnj1463  35052  iscvm  35253  mbfresfi  37667  sdclem2  37743  isdivrngo  37951  evlselvlem  42581  evlselv  42582  mzpcompact2lem  42746  diophrw  42754  eldioph2lem1  42755  eldioph2lem2  42756  eldioph3  42761  diophin  42767  diophrex  42770  rexrabdioph  42789  2rexfrabdioph  42791  3rexfrabdioph  42792  4rexfrabdioph  42793  6rexfrabdioph  42794  7rexfrabdioph  42795  eldioph4b  42806  pwssplit4  43085  dvnprodlem1  45951  dvnprodlem3  45953  ismea  46456  isome  46499