Theorem reseq1 5938

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

Syntax hints:   → wi 4   = wceq 1542  Vcvv 3429   ∩ cin 3888   × cxp 5629   ↾ cres 5633

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-in 3896  df-res 5643

This theorem is referenced by:  reseq1i  5940  reseq1d  5943  imaeq1  6020  fvtresfn  6950  eqfnun  6989  frrlem1  8236  frrlem13  8248  tfrlem12  8328  pmresg  8818  resixpfo  8884  mapunen  9084  fseqenlem1  9946  axdc3lem2  10373  axdc3lem4  10375  hashf1lem1  14417  lo1eq  15530  rlimeq  15531  symgfixfo  19414  lspextmo  21051  evlseu  22061  mdetunilem3  22579  mdetunilem4  22580  mdetunilem9  22585  lmbr  23223  ptuncnv  23772  iscau  25243  plyexmo  26279  relogf1o  26530  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  extvfvv  33678  extvfvcl  33680  eulerpartlemt  34515  eulerpartlemgv  34517  eulerpartlemn  34525  eulerpart  34526  bnj1385  34974  bnj66  35002  bnj1234  35155  bnj1326  35168  bnj1463  35197  iscvm  35441  mbfresfi  37987  sdclem2  38063  isdivrngo  38271  evlselvlem  43019  evlselv  43020  mzpcompact2lem  43183  diophrw  43191  eldioph2lem1  43192  eldioph2lem2  43193  eldioph3  43198  diophin  43204  diophrex  43207  rexrabdioph  43222  2rexfrabdioph  43224  3rexfrabdioph  43225  4rexfrabdioph  43226  6rexfrabdioph  43227  7rexfrabdioph  43228  eldioph4b  43239  pwssplit4  43517  dvnprodlem1  46374  dvnprodlem3  46376  ismea  46879  isome  46922