Theorem reseq1 5964

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

Syntax hints:   → wi 4   = wceq 1541  Vcvv 3470   ∩ cin 3940   × cxp 5664   ↾ cres 5668

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3430  df-in 3948  df-res 5678

This theorem is referenced by:  reseq1i  5966  reseq1d  5969  imaeq1  6041  fvtresfn  6983  frrlem1  8250  frrlem13  8262  wfrlem1OLD  8287  wfrlem3OLDa  8290  wfrlem15OLD  8302  tfrlem12  8368  pmresg  8844  resixpfo  8910  mapunen  9126  fseqenlem1  9998  axdc3lem2  10425  axdc3lem4  10427  axdc  10495  hashf1lem1  14394  hashf1lem1OLD  14395  lo1eq  15491  rlimeq  15492  symgfixfo  19268  lspextmo  20611  evlseu  21570  mdetunilem3  22040  mdetunilem4  22041  mdetunilem9  22046  lmbr  22686  ptuncnv  23235  iscau  24717  plyexmo  25750  relogf1o  25999  nosupprefixmo  27125  noinfprefixmo  27126  nosupcbv  27127  nosupno  27128  nosupdm  27129  nosupfv  27131  nosupres  27132  nosupbnd1lem1  27133  nosupbnd1lem3  27135  nosupbnd1lem5  27137  nosupbnd2  27141  noinfcbv  27142  noinfno  27143  noinfdm  27144  noinffv  27146  noinfres  27147  noinfbnd1lem1  27148  noinfbnd1lem3  27150  noinfbnd1lem5  27152  noinfbnd2  27156  eulerpartlemt  33185  eulerpartlemgv  33187  eulerpartlemn  33195  eulerpart  33196  bnj1385  33658  bnj66  33686  bnj1234  33839  bnj1326  33852  bnj1463  33881  iscvm  34065  mbfresfi  36322  eqfnun  36379  sdclem2  36399  isdivrngo  36607  mzpcompact2lem  41246  diophrw  41254  eldioph2lem1  41255  eldioph2lem2  41256  eldioph3  41261  diophin  41267  diophrex  41270  rexrabdioph  41289  2rexfrabdioph  41291  3rexfrabdioph  41292  4rexfrabdioph  41293  6rexfrabdioph  41294  7rexfrabdioph  41295  eldioph4b  41306  pwssplit4  41588  dvnprodlem1  44421  dvnprodlem3  44423  ismea  44926  isome  44969