Theorem reseq1 5118

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

Syntax hints:   -> wi 4   = wceq 1455   _Vcvv 3057   i^i cin 3415   X. cxp 4851   |` cres 4855

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-in 3423  df-res 4865

This theorem is referenced by:  reseq1i  5120  reseq1d  5123  imaeq1  5182  relcoi1OLD  5384  fvtresfn  5973  wfrlem1  7061  wfrlem3a  7064  wfrlem15  7076  tfrlem12  7133  pmresg  7525  resixpfo  7586  mapunen  7767  fseqenlem1  8481  axdc3lem2  8907  axdc3lem4  8909  axdc  8977  hashf1lem1  12651  lo1eq  13681  rlimeq  13682  symgfixfo  17129  lspextmo  18328  evlseu  18788  mdetunilem3  19688  mdetunilem4  19689  mdetunilem9  19694  lmbr  20323  ptuncnv  20871  iscau  22295  plyexmo  23315  relogf1o  23565  isdivrngo  26208  eulerpartlemt  29253  eulerpartlemgv  29255  eulerpartlemn  29263  eulerpart  29264  bnj1385  29693  bnj66  29720  bnj1234  29871  bnj1326  29884  bnj1463  29913  iscvm  30031  ghomgrplem  30356  trpredlem1  30517  trpredtr  30520  trpredmintr  30521  frrlem1  30563  nofulllem5  30644  mbfresfi  32032  eqfnun  32093  sdclem2  32116  mzpcompact2lem  35638  diophrw  35646  eldioph2lem1  35647  eldioph2lem2  35648  eldioph3  35653  diophin  35660  diophrex  35663  rexrabdioph  35682  2rexfrabdioph  35684  3rexfrabdioph  35685  4rexfrabdioph  35686  6rexfrabdioph  35687  7rexfrabdioph  35688  eldioph4b  35699  pwssplit4  35992  dvnprodlem1  37859  dvnprodlem3  37861  ismea  38327  isome  38353