Theorem reseq1 5812

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

Syntax hints:   → wi 4   = wceq 1538  Vcvv 3441   ∩ cin 3880   × cxp 5517   ↾ cres 5521

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-in 3888  df-res 5531

This theorem is referenced by:  reseq1i  5814  reseq1d  5817  imaeq1  5891  fvtresfn  6747  wfrlem1  7937  wfrlem3a  7940  wfrlem15  7952  tfrlem12  8008  pmresg  8417  resixpfo  8483  mapunen  8670  fseqenlem1  9435  axdc3lem2  9862  axdc3lem4  9864  axdc  9932  hashf1lem1  13809  lo1eq  14917  rlimeq  14918  symgfixfo  18559  lspextmo  19821  evlseu  20755  mdetunilem3  21219  mdetunilem4  21220  mdetunilem9  21225  lmbr  21863  ptuncnv  22412  iscau  23880  plyexmo  24909  relogf1o  25158  eulerpartlemt  31739  eulerpartlemgv  31741  eulerpartlemn  31749  eulerpart  31750  bnj1385  32214  bnj66  32242  bnj1234  32395  bnj1326  32408  bnj1463  32437  iscvm  32619  trpredlem1  33179  trpredtr  33182  trpredmintr  33183  frrlem1  33236  frrlem13  33248  noprefixmo  33315  nosupno  33316  nosupdm  33317  nosupfv  33319  nosupres  33320  nosupbnd1lem1  33321  nosupbnd1lem3  33323  nosupbnd1lem5  33325  nosupbnd2  33329  mbfresfi  35103  eqfnun  35160  sdclem2  35180  isdivrngo  35388  mzpcompact2lem  39692  diophrw  39700  eldioph2lem1  39701  eldioph2lem2  39702  eldioph3  39707  diophin  39713  diophrex  39716  rexrabdioph  39735  2rexfrabdioph  39737  3rexfrabdioph  39738  4rexfrabdioph  39739  6rexfrabdioph  39740  7rexfrabdioph  39741  eldioph4b  39752  pwssplit4  40033  dvnprodlem1  42588  dvnprodlem3  42590  ismea  43090  isome  43133