Theorem reseq1 5964

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  Vcvv 3451   ∩ cin 3898   × cxp 5649   ↾ cres 5653

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-in 3906  df-res 5663

This theorem is used by:  reseq1i  5966  reseq1d  5969  imaeq1  6049  fvtresfn  6988  eqfnun  7028  frrlem1  8288  frrlem13  8300  tfrlem12  8381  pmresg  8882  resixpfo  8948  mapunen  9149  fseqenlem1  10084  axdc3lem2  10510  axdc3lem4  10512  hashf1lem1  14580  lo1eq  15715  rlimeq  15716  symgfixfo  19633  lspextmo  21311  evlseu  22372  mdetunilem3  22909  mdetunilem4  22910  mdetunilem9  22915  lmbr  23556  ptuncnv  24106  iscau  25577  plyexmo  26618  relogf1o  26876  nosupprefixmo  28039  noinfprefixmo  28040  nosupcbv  28041  nosupno  28042  nosupdm  28043  nosupfv  28045  nosupres  28046  nosupbnd1lem1  28047  nosupbnd1lem3  28049  nosupbnd1lem5  28051  nosupbnd2  28055  noinfcbv  28056  noinfno  28057  noinfdm  28058  noinffv  28060  noinfres  28061  noinfbnd1lem1  28062  noinfbnd1lem3  28064  noinfbnd1lem5  28066  noinfbnd2  28070  extvfvv  34148  extvfvcl  34150  eulerpartlemt  34986  eulerpartlemgv  34988  eulerpartlemn  34996  eulerpart  34997  bnj1385  35445  bnj66  35473  bnj1234  35626  bnj1326  35639  bnj1463  35668  iscvm  35993  mbfresfi  38552  sdclem2  38644  isdivrngo  38852  evlselvlem  43578  evlselv  43579  mzpcompact2lem  43715  diophrw  43723  eldioph2lem1  43724  eldioph2lem2  43725  eldioph3  43730  diophin  43736  diophrex  43739  rexrabdioph  43754  2rexfrabdioph  43756  3rexfrabdioph  43757  4rexfrabdioph  43758  6rexfrabdioph  43759  7rexfrabdioph  43760  eldioph4b  43771  pwssplit4  44049  dvnprodlem1  46900  dvnprodlem3  46902  ismea  47405  isome  47448  tmachlem-agreeself  47890