Theorem reseq1 5936

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

Syntax hints:   → wi 4   = wceq 1541  Vcvv 3446   ∩ cin 3912   × cxp 5636   ↾ cres 5640

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 3406  df-in 3920  df-res 5650

This theorem is referenced by:  reseq1i  5938  reseq1d  5941  imaeq1  6013  fvtresfn  6955  frrlem1  8222  frrlem13  8234  wfrlem1OLD  8259  wfrlem3OLDa  8262  wfrlem15OLD  8274  tfrlem12  8340  pmresg  8815  resixpfo  8881  mapunen  9097  fseqenlem1  9969  axdc3lem2  10396  axdc3lem4  10398  axdc  10466  hashf1lem1  14365  hashf1lem1OLD  14366  lo1eq  15462  rlimeq  15463  symgfixfo  19235  lspextmo  20574  evlseu  21530  mdetunilem3  22000  mdetunilem4  22001  mdetunilem9  22006  lmbr  22646  ptuncnv  23195  iscau  24677  plyexmo  25710  relogf1o  25959  nosupprefixmo  27085  noinfprefixmo  27086  nosupcbv  27087  nosupno  27088  nosupdm  27089  nosupfv  27091  nosupres  27092  nosupbnd1lem1  27093  nosupbnd1lem3  27095  nosupbnd1lem5  27097  nosupbnd2  27101  noinfcbv  27102  noinfno  27103  noinfdm  27104  noinffv  27106  noinfres  27107  noinfbnd1lem1  27108  noinfbnd1lem3  27110  noinfbnd1lem5  27112  noinfbnd2  27116  eulerpartlemt  33060  eulerpartlemgv  33062  eulerpartlemn  33070  eulerpart  33071  bnj1385  33533  bnj66  33561  bnj1234  33714  bnj1326  33727  bnj1463  33756  iscvm  33940  mbfresfi  36197  eqfnun  36254  sdclem2  36274  isdivrngo  36482  mzpcompact2lem  41132  diophrw  41140  eldioph2lem1  41141  eldioph2lem2  41142  eldioph3  41147  diophin  41153  diophrex  41156  rexrabdioph  41175  2rexfrabdioph  41177  3rexfrabdioph  41178  4rexfrabdioph  41179  6rexfrabdioph  41180  7rexfrabdioph  41181  eldioph4b  41192  pwssplit4  41474  dvnprodlem1  44307  dvnprodlem3  44309  ismea  44812  isome  44855