Theorem reseq1 5932

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

Syntax hints:   → wi 4   = wceq 1542  Vcvv 3430   ∩ cin 3889   × cxp 5622   ↾ cres 5626

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-in 3897  df-res 5636

This theorem is referenced by:  reseq1i  5934  reseq1d  5937  imaeq1  6014  fvtresfn  6944  eqfnun  6983  frrlem1  8229  frrlem13  8241  tfrlem12  8321  pmresg  8811  resixpfo  8877  mapunen  9077  fseqenlem1  9937  axdc3lem2  10364  axdc3lem4  10366  hashf1lem1  14408  lo1eq  15521  rlimeq  15522  symgfixfo  19405  lspextmo  21043  evlseu  22071  mdetunilem3  22589  mdetunilem4  22590  mdetunilem9  22595  lmbr  23233  ptuncnv  23782  iscau  25253  plyexmo  26290  relogf1o  26543  nosupprefixmo  27678  noinfprefixmo  27679  nosupcbv  27680  nosupno  27681  nosupdm  27682  nosupfv  27684  nosupres  27685  nosupbnd1lem1  27686  nosupbnd1lem3  27688  nosupbnd1lem5  27690  nosupbnd2  27694  noinfcbv  27695  noinfno  27696  noinfdm  27697  noinffv  27699  noinfres  27700  noinfbnd1lem1  27701  noinfbnd1lem3  27703  noinfbnd1lem5  27705  noinfbnd2  27709  extvfvv  33693  extvfvcl  33695  eulerpartlemt  34531  eulerpartlemgv  34533  eulerpartlemn  34541  eulerpart  34542  bnj1385  34990  bnj66  35018  bnj1234  35171  bnj1326  35184  bnj1463  35213  iscvm  35457  mbfresfi  38001  sdclem2  38077  isdivrngo  38285  evlselvlem  43033  evlselv  43034  mzpcompact2lem  43197  diophrw  43205  eldioph2lem1  43206  eldioph2lem2  43207  eldioph3  43212  diophin  43218  diophrex  43221  rexrabdioph  43240  2rexfrabdioph  43242  3rexfrabdioph  43243  4rexfrabdioph  43244  6rexfrabdioph  43245  7rexfrabdioph  43246  eldioph4b  43257  pwssplit4  43535  dvnprodlem1  46392  dvnprodlem3  46394  ismea  46897  isome  46940