Theorem reseq1 5119

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 3663	. 2 |- ( A = B -> ( A i^i ( C X. _V ) ) = ( B i^i ( C X. _V ) ) )
2		df-res 4866	. 2 |- ( A |` C ) = ( A i^i ( C X. _V ) )
3		df-res 4866	. 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 1437   _Vcvv 3087   i^i cin 3441   X. cxp 4852   |` cres 4856

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-v 3089  df-in 3449  df-res 4866

This theorem is referenced by:  reseq1i  5121  reseq1d  5124  imaeq1  5183  relcoi1OLD  5385  fvtresfn  5966  wfrlem1  7043  wfrlem3a  7046  wfrlem15  7058  tfrlem12  7115  pmresg  7507  resixpfo  7568  mapunen  7747  fseqenlem1  8453  axdc3lem2  8879  axdc3lem4  8881  axdc  8949  hashf1lem1  12613  lo1eq  13610  rlimeq  13611  symgfixfo  17031  lspextmo  18214  evlseu  18674  mdetunilem3  19570  mdetunilem4  19571  mdetunilem9  19576  lmbr  20205  ptuncnv  20753  iscau  22139  plyexmo  23134  relogf1o  23381  isdivrngo  26004  eulerpartlemt  29030  eulerpartlemgv  29032  eulerpartlemn  29040  eulerpart  29041  bnj1385  29432  bnj66  29459  bnj1234  29610  bnj1326  29623  bnj1463  29652  iscvm  29770  ghomgrplem  30095  trpredlem1  30255  trpredtr  30258  trpredmintr  30259  frrlem1  30301  nofulllem5  30380  mbfresfi  31691  eqfnun  31752  sdclem2  31775  mzpcompact2lem  35302  diophrw  35310  eldioph2lem1  35311  eldioph2lem2  35312  eldioph3  35317  diophin  35324  diophrex  35327  rexrabdioph  35346  2rexfrabdioph  35348  3rexfrabdioph  35349  4rexfrabdioph  35350  6rexfrabdioph  35351  7rexfrabdioph  35352  eldioph4b  35363  pwssplit4  35653  dvnprodlem1  37390  dvnprodlem3  37392  ismea  37798  isome  37824