Theorem reseq1 5820

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

Assertion

Ref	Expression
reseq1	⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))

Proof of Theorem reseq1

Step	Hyp	Ref	Expression
1		ineq1 4097	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ (𝐶 × V)) = (𝐵 ∩ (𝐶 × V)))
2		df-res 5538	. 2 ⊢ (𝐴 ↾ 𝐶) = (𝐴 ∩ (𝐶 × V))
3		df-res 5538	. 2 ⊢ (𝐵 ↾ 𝐶) = (𝐵 ∩ (𝐶 × V))
4	1, 2, 3	3eqtr4g 2799	1 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))

Syntax hints:   → wi 4   = wceq 1542  Vcvv 3399   ∩ cin 3843   × cxp 5524   ↾ cres 5528

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-rab 3063  df-in 3851  df-res 5538

This theorem is referenced by:  reseq1i  5822  reseq1d  5825  imaeq1  5899  fvtresfn  6780  wfrlem1  7986  wfrlem3a  7989  wfrlem15  8001  tfrlem12  8057  pmresg  8483  resixpfo  8549  mapunen  8739  fseqenlem1  9527  axdc3lem2  9954  axdc3lem4  9956  axdc  10024  hashf1lem1  13909  hashf1lem1OLD  13910  lo1eq  15018  rlimeq  15019  symgfixfo  18688  lspextmo  19950  evlseu  20900  mdetunilem3  21368  mdetunilem4  21369  mdetunilem9  21374  lmbr  22012  ptuncnv  22561  iscau  24031  plyexmo  25064  relogf1o  25313  eulerpartlemt  31911  eulerpartlemgv  31913  eulerpartlemn  31921  eulerpart  31922  bnj1385  32386  bnj66  32414  bnj1234  32567  bnj1326  32580  bnj1463  32609  iscvm  32795  trpredlem1  33374  trpredtr  33377  trpredmintr  33378  frrlem1  33446  frrlem13  33458  nosupprefixmo  33549  noinfprefixmo  33550  nosupcbv  33551  nosupno  33552  nosupdm  33553  nosupfv  33555  nosupres  33556  nosupbnd1lem1  33557  nosupbnd1lem3  33559  nosupbnd1lem5  33561  nosupbnd2  33565  noinfcbv  33566  noinfno  33567  noinfdm  33568  noinffv  33570  noinfres  33571  noinfbnd1lem1  33572  noinfbnd1lem3  33574  noinfbnd1lem5  33576  noinfbnd2  33580  mbfresfi  35469  eqfnun  35526  sdclem2  35546  isdivrngo  35754  mzpcompact2lem  40168  diophrw  40176  eldioph2lem1  40177  eldioph2lem2  40178  eldioph3  40183  diophin  40189  diophrex  40192  rexrabdioph  40211  2rexfrabdioph  40213  3rexfrabdioph  40214  4rexfrabdioph  40215  6rexfrabdioph  40216  7rexfrabdioph  40217  eldioph4b  40228  pwssplit4  40509  dvnprodlem1  43052  dvnprodlem3  43054  ismea  43554  isome  43597