Theorem reseq1 5962

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

Syntax hints:   → wi 4   = wceq 1541  Vcvv 3469   ∩ cin 3938   × cxp 5662   ↾ cres 5666

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3429  df-in 3946  df-res 5676

This theorem is referenced by:  reseq1i  5964  reseq1d  5967  imaeq1  6039  fvtresfn  6981  frrlem1  8248  frrlem13  8260  wfrlem1OLD  8285  wfrlem3OLDa  8288  wfrlem15OLD  8300  tfrlem12  8366  pmresg  8842  resixpfo  8908  mapunen  9124  fseqenlem1  9996  axdc3lem2  10423  axdc3lem4  10425  axdc  10493  hashf1lem1  14392  hashf1lem1OLD  14393  lo1eq  15489  rlimeq  15490  symgfixfo  19266  lspextmo  20609  evlseu  21568  mdetunilem3  22038  mdetunilem4  22039  mdetunilem9  22044  lmbr  22684  ptuncnv  23233  iscau  24715  plyexmo  25748  relogf1o  25997  nosupprefixmo  27123  noinfprefixmo  27124  nosupcbv  27125  nosupno  27126  nosupdm  27127  nosupfv  27129  nosupres  27130  nosupbnd1lem1  27131  nosupbnd1lem3  27133  nosupbnd1lem5  27135  nosupbnd2  27139  noinfcbv  27140  noinfno  27141  noinfdm  27142  noinffv  27144  noinfres  27145  noinfbnd1lem1  27146  noinfbnd1lem3  27148  noinfbnd1lem5  27150  noinfbnd2  27154  eulerpartlemt  33136  eulerpartlemgv  33138  eulerpartlemn  33146  eulerpart  33147  bnj1385  33609  bnj66  33637  bnj1234  33790  bnj1326  33803  bnj1463  33832  iscvm  34016  mbfresfi  36273  eqfnun  36330  sdclem2  36350  isdivrngo  36558  mzpcompact2lem  41197  diophrw  41205  eldioph2lem1  41206  eldioph2lem2  41207  eldioph3  41212  diophin  41218  diophrex  41221  rexrabdioph  41240  2rexfrabdioph  41242  3rexfrabdioph  41243  4rexfrabdioph  41244  6rexfrabdioph  41245  7rexfrabdioph  41246  eldioph4b  41257  pwssplit4  41539  dvnprodlem1  44372  dvnprodlem3  44374  ismea  44877  isome  44920