Theorem reseq1 5099

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 3540	. 2 |- ( A = B -> ( A i^i ( C X. _V ) ) = ( B i^i ( C X. _V ) ) )
2		df-res 4847	. 2 |- ( A |` C ) = ( A i^i ( C X. _V ) )
3		df-res 4847	. 2 |- ( B |` C ) = ( B i^i ( C X. _V ) )
4	1, 2, 3	3eqtr4g 2495	1 |- ( A = B -> ( A |` C ) = ( B |` C ) )

Syntax hints:   -> wi 4   = wceq 1369   _Vcvv 2967   i^i cin 3322   X. cxp 4833   |` cres 4837

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-in 3330  df-res 4847

This theorem is referenced by:  reseq1i  5101  reseq1d  5104  imaeq1  5159  relcoi1  5361  fvtresfn  5770  tfrlem12  6840  pmresg  7232  resixpfo  7293  mapunen  7472  fseqenlem1  8186  axdc3lem2  8612  axdc3lem4  8614  axdc  8682  hashf1lem1  12200  lo1eq  13038  rlimeq  13039  symgfixfvh  15932  symgfixfo  15936  lspextmo  17114  evlseu  17577  mdetunilem3  18395  mdetunilem4  18396  mdetunilem9  18401  lmbr  18837  ptuncnv  19355  iscau  20762  plyexmo  21754  relogf1o  21993  isdivrngo  23869  eulerpartlemt  26706  eulerpartgbij  26707  eulerpartlemgv  26708  eulerpartlemn  26716  eulerpart  26717  iscvm  27100  ghomgrplem  27259  trpredlem1  27642  trpredtr  27645  trpredmintr  27646  wfrlem1  27675  wfrlem15  27689  frrlem1  27719  nofulllem5  27798  mbfresfi  28391  eqfnun  28568  sdclem2  28591  mzpcompact2lem  29041  diophrw  29050  eldioph2lem1  29051  eldioph2lem2  29052  eldioph3  29057  diophin  29064  diophrex  29067  rexrabdioph  29085  2rexfrabdioph  29087  3rexfrabdioph  29088  4rexfrabdioph  29089  6rexfrabdioph  29090  7rexfrabdioph  29091  eldioph4b  29103  pwssplit4  29395  bnj1385  31713  bnj66  31740  bnj1234  31891  bnj1326  31904  bnj1463  31933