Theorem reseq1 5993

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 4220	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ (𝐶 × V)) = (𝐵 ∩ (𝐶 × V)))
2		df-res 5700	. 2 ⊢ (𝐴 ↾ 𝐶) = (𝐴 ∩ (𝐶 × V))
3		df-res 5700	. 2 ⊢ (𝐵 ↾ 𝐶) = (𝐵 ∩ (𝐶 × V))
4	1, 2, 3	3eqtr4g 2799	1 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))

Syntax hints:   → wi 4   = wceq 1536  Vcvv 3477   ∩ cin 3961   × cxp 5686   ↾ cres 5690

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-in 3969  df-res 5700

This theorem is referenced by:  reseq1i  5995  reseq1d  5998  imaeq1  6074  fvtresfn  7017  eqfnun  7056  frrlem1  8309  frrlem13  8321  wfrlem1OLD  8346  wfrlem3OLDa  8349  wfrlem15OLD  8361  tfrlem12  8427  pmresg  8908  resixpfo  8974  mapunen  9184  fseqenlem1  10061  axdc3lem2  10488  axdc3lem4  10490  axdc  10558  hashf1lem1  14490  lo1eq  15600  rlimeq  15601  symgfixfo  19471  lspextmo  21072  evlseu  22124  mdetunilem3  22635  mdetunilem4  22636  mdetunilem9  22641  lmbr  23281  ptuncnv  23830  iscau  25323  plyexmo  26369  relogf1o  26622  nosupprefixmo  27759  noinfprefixmo  27760  nosupcbv  27761  nosupno  27762  nosupdm  27763  nosupfv  27765  nosupres  27766  nosupbnd1lem1  27767  nosupbnd1lem3  27769  nosupbnd1lem5  27771  nosupbnd2  27775  noinfcbv  27776  noinfno  27777  noinfdm  27778  noinffv  27780  noinfres  27781  noinfbnd1lem1  27782  noinfbnd1lem3  27784  noinfbnd1lem5  27786  noinfbnd2  27790  eulerpartlemt  34352  eulerpartlemgv  34354  eulerpartlemn  34362  eulerpart  34363  bnj1385  34824  bnj66  34852  bnj1234  35005  bnj1326  35018  bnj1463  35047  iscvm  35243  mbfresfi  37652  sdclem2  37728  isdivrngo  37936  evlselvlem  42572  evlselv  42573  mzpcompact2lem  42738  diophrw  42746  eldioph2lem1  42747  eldioph2lem2  42748  eldioph3  42753  diophin  42759  diophrex  42762  rexrabdioph  42781  2rexfrabdioph  42783  3rexfrabdioph  42784  4rexfrabdioph  42785  6rexfrabdioph  42786  7rexfrabdioph  42787  eldioph4b  42798  pwssplit4  43077  dvnprodlem1  45901  dvnprodlem3  45903  ismea  46406  isome  46449