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

Syntax hints:   → wi 4   = wceq 1541  Vcvv 3440   ∩ cin 3900   × cxp 5622   ↾ cres 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-in 3908  df-res 5636

This theorem is referenced by:  reseq1i  5934  reseq1d  5937  imaeq1  6014  fvtresfn  6943  eqfnun  6982  frrlem1  8228  frrlem13  8240  tfrlem12  8320  pmresg  8808  resixpfo  8874  mapunen  9074  fseqenlem1  9934  axdc3lem2  10361  axdc3lem4  10363  hashf1lem1  14378  lo1eq  15491  rlimeq  15492  symgfixfo  19368  lspextmo  21008  evlseu  22038  mdetunilem3  22558  mdetunilem4  22559  mdetunilem9  22564  lmbr  23202  ptuncnv  23751  iscau  25232  plyexmo  26277  relogf1o  26531  nosupprefixmo  27668  noinfprefixmo  27669  nosupcbv  27670  nosupno  27671  nosupdm  27672  nosupfv  27674  nosupres  27675  nosupbnd1lem1  27676  nosupbnd1lem3  27678  nosupbnd1lem5  27680  nosupbnd2  27684  noinfcbv  27685  noinfno  27686  noinfdm  27687  noinffv  27689  noinfres  27690  noinfbnd1lem1  27691  noinfbnd1lem3  27693  noinfbnd1lem5  27695  noinfbnd2  27699  extvfvv  33699  extvfvcl  33701  eulerpartlemt  34528  eulerpartlemgv  34530  eulerpartlemn  34538  eulerpart  34539  bnj1385  34988  bnj66  35016  bnj1234  35169  bnj1326  35182  bnj1463  35211  iscvm  35453  mbfresfi  37863  sdclem2  37939  isdivrngo  38147  evlselvlem  42825  evlselv  42826  mzpcompact2lem  42989  diophrw  42997  eldioph2lem1  42998  eldioph2lem2  42999  eldioph3  43004  diophin  43010  diophrex  43013  rexrabdioph  43032  2rexfrabdioph  43034  3rexfrabdioph  43035  4rexfrabdioph  43036  6rexfrabdioph  43037  7rexfrabdioph  43038  eldioph4b  43049  pwssplit4  43327  dvnprodlem1  46186  dvnprodlem3  46188  ismea  46691  isome  46734