Theorem reseq1 6003

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

Syntax hints:   → wi 4   = wceq 1537  Vcvv 3488   ∩ cin 3975   × cxp 5698   ↾ cres 5702

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-in 3983  df-res 5712

This theorem is referenced by:  reseq1i  6005  reseq1d  6008  imaeq1  6084  fvtresfn  7031  eqfnun  7070  frrlem1  8327  frrlem13  8339  wfrlem1OLD  8364  wfrlem3OLDa  8367  wfrlem15OLD  8379  tfrlem12  8445  pmresg  8928  resixpfo  8994  mapunen  9212  fseqenlem1  10093  axdc3lem2  10520  axdc3lem4  10522  axdc  10590  hashf1lem1  14504  lo1eq  15614  rlimeq  15615  symgfixfo  19481  lspextmo  21078  evlseu  22130  mdetunilem3  22641  mdetunilem4  22642  mdetunilem9  22647  lmbr  23287  ptuncnv  23836  iscau  25329  plyexmo  26373  relogf1o  26626  nosupprefixmo  27763  noinfprefixmo  27764  nosupcbv  27765  nosupno  27766  nosupdm  27767  nosupfv  27769  nosupres  27770  nosupbnd1lem1  27771  nosupbnd1lem3  27773  nosupbnd1lem5  27775  nosupbnd2  27779  noinfcbv  27780  noinfno  27781  noinfdm  27782  noinffv  27784  noinfres  27785  noinfbnd1lem1  27786  noinfbnd1lem3  27788  noinfbnd1lem5  27790  noinfbnd2  27794  eulerpartlemt  34336  eulerpartlemgv  34338  eulerpartlemn  34346  eulerpart  34347  bnj1385  34808  bnj66  34836  bnj1234  34989  bnj1326  35002  bnj1463  35031  iscvm  35227  mbfresfi  37626  sdclem2  37702  isdivrngo  37910  evlselvlem  42541  evlselv  42542  mzpcompact2lem  42707  diophrw  42715  eldioph2lem1  42716  eldioph2lem2  42717  eldioph3  42722  diophin  42728  diophrex  42731  rexrabdioph  42750  2rexfrabdioph  42752  3rexfrabdioph  42753  4rexfrabdioph  42754  6rexfrabdioph  42755  7rexfrabdioph  42756  eldioph4b  42767  pwssplit4  43046  dvnprodlem1  45867  dvnprodlem3  45869  ismea  46372  isome  46415