Theorem reseq1 5215

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

Syntax hints:   -> wi 4   = wceq 1370   _Vcvv 3078   i^i cin 3438   X. cxp 4949   |` cres 4953

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3080  df-in 3446  df-res 4963

This theorem is referenced by:  reseq1i  5217  reseq1d  5220  imaeq1  5275  relcoi1  5477  fvtresfn  5887  tfrlem12  6961  pmresg  7353  resixpfo  7414  mapunen  7593  fseqenlem1  8308  axdc3lem2  8734  axdc3lem4  8736  axdc  8804  hashf1lem1  12329  lo1eq  13167  rlimeq  13168  symgfixfvh  16063  symgfixfo  16067  lspextmo  17263  evlseu  17729  mdetunilem3  18555  mdetunilem4  18556  mdetunilem9  18561  lmbr  18997  ptuncnv  19515  iscau  20922  plyexmo  21915  relogf1o  22154  isdivrngo  24090  eulerpartlemt  26918  eulerpartgbij  26919  eulerpartlemgv  26920  eulerpartlemn  26928  eulerpart  26929  iscvm  27312  ghomgrplem  27472  trpredlem1  27855  trpredtr  27858  trpredmintr  27859  wfrlem1  27888  wfrlem15  27902  frrlem1  27932  nofulllem5  28011  mbfresfi  28606  eqfnun  28783  sdclem2  28806  mzpcompact2lem  29256  diophrw  29265  eldioph2lem1  29266  eldioph2lem2  29267  eldioph3  29272  diophin  29279  diophrex  29282  rexrabdioph  29300  2rexfrabdioph  29302  3rexfrabdioph  29303  4rexfrabdioph  29304  6rexfrabdioph  29305  7rexfrabdioph  29306  eldioph4b  29318  pwssplit4  29610  bnj1385  32178  bnj66  32205  bnj1234  32356  bnj1326  32369  bnj1463  32398