Theorem reseq1 5940

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

Syntax hints:   → wi 4   = wceq 1542  Vcvv 3442   ∩ cin 3902   × cxp 5630   ↾ cres 5634

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 3402  df-in 3910  df-res 5644

This theorem is referenced by:  reseq1i  5942  reseq1d  5945  imaeq1  6022  fvtresfn  6952  eqfnun  6991  frrlem1  8238  frrlem13  8250  tfrlem12  8330  pmresg  8820  resixpfo  8886  mapunen  9086  fseqenlem1  9946  axdc3lem2  10373  axdc3lem4  10375  hashf1lem1  14390  lo1eq  15503  rlimeq  15504  symgfixfo  19380  lspextmo  21020  evlseu  22050  mdetunilem3  22570  mdetunilem4  22571  mdetunilem9  22576  lmbr  23214  ptuncnv  23763  iscau  25244  plyexmo  26289  relogf1o  26543  nosupprefixmo  27680  noinfprefixmo  27681  nosupcbv  27682  nosupno  27683  nosupdm  27684  nosupfv  27686  nosupres  27687  nosupbnd1lem1  27688  nosupbnd1lem3  27690  nosupbnd1lem5  27692  nosupbnd2  27696  noinfcbv  27697  noinfno  27698  noinfdm  27699  noinffv  27701  noinfres  27702  noinfbnd1lem1  27703  noinfbnd1lem3  27705  noinfbnd1lem5  27707  noinfbnd2  27711  extvfvv  33710  extvfvcl  33712  eulerpartlemt  34548  eulerpartlemgv  34550  eulerpartlemn  34558  eulerpart  34559  bnj1385  35007  bnj66  35035  bnj1234  35188  bnj1326  35201  bnj1463  35230  iscvm  35472  mbfresfi  37911  sdclem2  37987  isdivrngo  38195  evlselvlem  42938  evlselv  42939  mzpcompact2lem  43102  diophrw  43110  eldioph2lem1  43111  eldioph2lem2  43112  eldioph3  43117  diophin  43123  diophrex  43126  rexrabdioph  43145  2rexfrabdioph  43147  3rexfrabdioph  43148  4rexfrabdioph  43149  6rexfrabdioph  43150  7rexfrabdioph  43151  eldioph4b  43162  pwssplit4  43440  dvnprodlem1  46298  dvnprodlem3  46300  ismea  46803  isome  46846