Theorem reseq1 5960

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

Syntax hints:   → wi 4   = wceq 1540  Vcvv 3459   ∩ cin 3925   × cxp 5652   ↾ cres 5656

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-in 3933  df-res 5666

This theorem is referenced by:  reseq1i  5962  reseq1d  5965  imaeq1  6042  fvtresfn  6988  eqfnun  7027  frrlem1  8285  frrlem13  8297  wfrlem1OLD  8322  wfrlem3OLDa  8325  wfrlem15OLD  8337  tfrlem12  8403  pmresg  8884  resixpfo  8950  mapunen  9160  fseqenlem1  10038  axdc3lem2  10465  axdc3lem4  10467  hashf1lem1  14473  lo1eq  15584  rlimeq  15585  symgfixfo  19420  lspextmo  21014  evlseu  22041  mdetunilem3  22552  mdetunilem4  22553  mdetunilem9  22558  lmbr  23196  ptuncnv  23745  iscau  25228  plyexmo  26273  relogf1o  26527  nosupprefixmo  27664  noinfprefixmo  27665  nosupcbv  27666  nosupno  27667  nosupdm  27668  nosupfv  27670  nosupres  27671  nosupbnd1lem1  27672  nosupbnd1lem3  27674  nosupbnd1lem5  27676  nosupbnd2  27680  noinfcbv  27681  noinfno  27682  noinfdm  27683  noinffv  27685  noinfres  27686  noinfbnd1lem1  27687  noinfbnd1lem3  27689  noinfbnd1lem5  27691  noinfbnd2  27695  eulerpartlemt  34403  eulerpartlemgv  34405  eulerpartlemn  34413  eulerpart  34414  bnj1385  34863  bnj66  34891  bnj1234  35044  bnj1326  35057  bnj1463  35086  iscvm  35281  mbfresfi  37690  sdclem2  37766  isdivrngo  37974  evlselvlem  42609  evlselv  42610  mzpcompact2lem  42774  diophrw  42782  eldioph2lem1  42783  eldioph2lem2  42784  eldioph3  42789  diophin  42795  diophrex  42798  rexrabdioph  42817  2rexfrabdioph  42819  3rexfrabdioph  42820  4rexfrabdioph  42821  6rexfrabdioph  42822  7rexfrabdioph  42823  eldioph4b  42834  pwssplit4  43113  dvnprodlem1  45975  dvnprodlem3  45977  ismea  46480  isome  46523