Theorem reseq1 5963

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  Vcvv 3450   ∩ cin 4089   × cxp 5648   ↾ cres 5652

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-in 4091  df-res 5662

This theorem is used by:  reseq1i  5965  reseq1d  5968  imaeq1  6046  fvtresfn  6996  eqfnun  7036  frrlem1  8307  frrlem13  8319  tfrlem12  8400  pmresg  8901  resixpfo  8967  mapunen  9168  fseqenlem1  10106  axdc3lem2  10532  axdc3lem4  10534  hashf1lem1  14603  lo1eq  15740  rlimeq  15741  symgfixfo  19658  lspextmo  21336  evlseu  22397  mdetunilem3  22934  mdetunilem4  22935  mdetunilem9  22940  lmbr  23581  ptuncnv  24131  iscau  25602  plyexmo  26641  relogf1o  26899  nosupprefixmo  28062  noinfprefixmo  28063  nosupcbv  28064  nosupno  28065  nosupdm  28066  nosupfv  28068  nosupres  28069  nosupbnd1lem1  28070  nosupbnd1lem3  28072  nosupbnd1lem5  28074  nosupbnd2  28078  noinfcbv  28079  noinfno  28080  noinfdm  28081  noinffv  28083  noinfres  28084  noinfbnd1lem1  28085  noinfbnd1lem3  28087  noinfbnd1lem5  28089  noinfbnd2  28093  extvfvv  34212  extvfvcl  34214  eulerpartlemt  35049  eulerpartlemgv  35051  eulerpartlemn  35059  eulerpart  35060  bnj1385  35508  bnj66  35536  bnj1234  35689  bnj1326  35702  bnj1463  35731  iscvm  36110  mbfresfi  38677  sdclem2  38769  isdivrngo  38977  evlselvlem  43709  evlselv  43710  mzpcompact2lem  43855  diophrw  43863  eldioph2lem1  43864  eldioph2lem2  43865  eldioph3  43870  diophin  43876  diophrex  43879  rexrabdioph  43894  2rexfrabdioph  43896  3rexfrabdioph  43897  4rexfrabdioph  43898  6rexfrabdioph  43899  7rexfrabdioph  43900  eldioph4b  43911  pwssplit4  44184  dvnprodlem1  47049  dvnprodlem3  47051  ismea  47554  isome  47597  tmachlem-agreeself  48039