Theorem reseq1 5973

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

Syntax hints:   → wi 4   = wceq 1534  Vcvv 3469   ∩ cin 3943   × cxp 5670   ↾ cres 5674

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-rab 3428  df-in 3951  df-res 5684

This theorem is referenced by:  reseq1i  5975  reseq1d  5978  imaeq1  6052  fvtresfn  7001  eqfnun  7040  frrlem1  8285  frrlem13  8297  wfrlem1OLD  8322  wfrlem3OLDa  8325  wfrlem15OLD  8337  tfrlem12  8403  pmresg  8880  resixpfo  8946  mapunen  9162  fseqenlem1  10039  axdc3lem2  10466  axdc3lem4  10468  axdc  10536  hashf1lem1  14439  hashf1lem1OLD  14440  lo1eq  15536  rlimeq  15537  symgfixfo  19385  lspextmo  20930  evlseu  22016  mdetunilem3  22503  mdetunilem4  22504  mdetunilem9  22509  lmbr  23149  ptuncnv  23698  iscau  25191  plyexmo  26235  relogf1o  26487  nosupprefixmo  27620  noinfprefixmo  27621  nosupcbv  27622  nosupno  27623  nosupdm  27624  nosupfv  27626  nosupres  27627  nosupbnd1lem1  27628  nosupbnd1lem3  27630  nosupbnd1lem5  27632  nosupbnd2  27636  noinfcbv  27637  noinfno  27638  noinfdm  27639  noinffv  27641  noinfres  27642  noinfbnd1lem1  27643  noinfbnd1lem3  27645  noinfbnd1lem5  27647  noinfbnd2  27651  eulerpartlemt  33927  eulerpartlemgv  33929  eulerpartlemn  33937  eulerpart  33938  bnj1385  34399  bnj66  34427  bnj1234  34580  bnj1326  34593  bnj1463  34622  iscvm  34805  mbfresfi  37074  sdclem2  37150  isdivrngo  37358  evlselvlem  41741  evlselv  41742  mzpcompact2lem  42093  diophrw  42101  eldioph2lem1  42102  eldioph2lem2  42103  eldioph3  42108  diophin  42114  diophrex  42117  rexrabdioph  42136  2rexfrabdioph  42138  3rexfrabdioph  42139  4rexfrabdioph  42140  6rexfrabdioph  42141  7rexfrabdioph  42142  eldioph4b  42153  pwssplit4  42435  dvnprodlem1  45257  dvnprodlem3  45259  ismea  45762  isome  45805