Theorem reseq1 5970

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  Vcvv 3453   ∩ cin 3901   × cxp 5657   ↾ cres 5661

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 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-in 3909  df-res 5671

This theorem is used by:  reseq1i  5972  reseq1d  5975  imaeq1  6055  fvtresfn  6993  eqfnun  7033  frrlem1  8289  frrlem13  8301  tfrlem12  8382  pmresg  8881  resixpfo  8947  mapunen  9148  fseqenlem1  10031  axdc3lem2  10457  axdc3lem4  10459  hashf1lem1  14524  lo1eq  15659  rlimeq  15660  symgfixfo  19572  lspextmo  21246  evlseu  22305  mdetunilem3  22842  mdetunilem4  22843  mdetunilem9  22848  lmbr  23489  ptuncnv  24039  iscau  25510  plyexmo  26552  relogf1o  26811  nosupprefixmo  27944  noinfprefixmo  27945  nosupcbv  27946  nosupno  27947  nosupdm  27948  nosupfv  27950  nosupres  27951  nosupbnd1lem1  27952  nosupbnd1lem3  27954  nosupbnd1lem5  27956  nosupbnd2  27960  noinfcbv  27961  noinfno  27962  noinfdm  27963  noinffv  27965  noinfres  27966  noinfbnd1lem1  27967  noinfbnd1lem3  27969  noinfbnd1lem5  27971  noinfbnd2  27975  extvfvv  34052  extvfvcl  34054  eulerpartlemt  34890  eulerpartlemgv  34892  eulerpartlemn  34900  eulerpart  34901  bnj1385  35349  bnj66  35377  bnj1234  35530  bnj1326  35543  bnj1463  35572  iscvm  35846  mbfresfi  38423  sdclem2  38500  isdivrngo  38708  evlselvlem  43442  evlselv  43443  mzpcompact2lem  43604  diophrw  43612  eldioph2lem1  43613  eldioph2lem2  43614  eldioph3  43619  diophin  43625  diophrex  43628  rexrabdioph  43643  2rexfrabdioph  43645  3rexfrabdioph  43646  4rexfrabdioph  43647  6rexfrabdioph  43648  7rexfrabdioph  43649  eldioph4b  43660  pwssplit4  43938  dvnprodlem1  46782  dvnprodlem3  46784  ismea  47287  isome  47330  tmachlem-agreeself  47772