Theorem reseq1 5266

Description: Equality theorem for restrictions. (Contributed by NM, 7-Aug-1994.)

Assertion

Ref	Expression
reseq1	|- ( A = B -> ( A |` C ) = ( B |` C ) )

Proof of Theorem reseq1

Step	Hyp	Ref	Expression
1		ineq1 3693	. 2 |- ( A = B -> ( A i^i ( C X. _V ) ) = ( B i^i ( C X. _V ) ) )
2		df-res 5011	. 2 |- ( A |` C ) = ( A i^i ( C X. _V ) )
3		df-res 5011	. 2 |- ( B |` C ) = ( B i^i ( C X. _V ) )
4	1, 2, 3	3eqtr4g 2533	1 |- ( A = B -> ( A |` C ) = ( B |` C ) )

Syntax hints:   -> wi 4   = wceq 1379   _Vcvv 3113   i^i cin 3475   X. cxp 4997   |` cres 5001

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-in 3483  df-res 5011

This theorem is referenced by:  reseq1i  5268  reseq1d  5271  imaeq1  5331  relcoi1  5535  fvtresfn  5950  tfrlem12  7058  pmresg  7446  resixpfo  7507  mapunen  7686  fseqenlem1  8404  axdc3lem2  8830  axdc3lem4  8832  axdc  8900  hashf1lem1  12469  lo1eq  13353  rlimeq  13354  symgfixfvh  16263  symgfixfo  16267  lspextmo  17497  evlseu  17972  mdetunilem3  18899  mdetunilem4  18900  mdetunilem9  18905  lmbr  19541  ptuncnv  20059  iscau  21466  plyexmo  22459  relogf1o  22698  isdivrngo  25125  eulerpartlemt  27966  eulerpartgbij  27967  eulerpartlemgv  27968  eulerpartlemn  27976  eulerpart  27977  iscvm  28360  ghomgrplem  28520  trpredlem1  28903  trpredtr  28906  trpredmintr  28907  wfrlem1  28936  wfrlem15  28950  frrlem1  28980  nofulllem5  29059  mbfresfi  29654  eqfnun  29831  sdclem2  29854  mzpcompact2lem  30304  diophrw  30312  eldioph2lem1  30313  eldioph2lem2  30314  eldioph3  30319  diophin  30326  diophrex  30329  rexrabdioph  30347  2rexfrabdioph  30349  3rexfrabdioph  30350  4rexfrabdioph  30351  6rexfrabdioph  30352  7rexfrabdioph  30353  eldioph4b  30365  pwssplit4  30655  bnj1385  32979  bnj66  33006  bnj1234  33157  bnj1326  33170  bnj1463  33199