Theorem reseq1 5922

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

Syntax hints:   → wi 4   = wceq 1541  Vcvv 3436   ∩ cin 3901   × cxp 5614   ↾ cres 5618

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-in 3909  df-res 5628

This theorem is referenced by:  reseq1i  5924  reseq1d  5927  imaeq1  6004  fvtresfn  6931  eqfnun  6970  frrlem1  8216  frrlem13  8228  tfrlem12  8308  pmresg  8794  resixpfo  8860  mapunen  9059  fseqenlem1  9912  axdc3lem2  10339  axdc3lem4  10341  hashf1lem1  14359  lo1eq  15472  rlimeq  15473  symgfixfo  19349  lspextmo  20988  evlseu  22016  mdetunilem3  22527  mdetunilem4  22528  mdetunilem9  22533  lmbr  23171  ptuncnv  23720  iscau  25201  plyexmo  26246  relogf1o  26500  nosupprefixmo  27637  noinfprefixmo  27638  nosupcbv  27639  nosupno  27640  nosupdm  27641  nosupfv  27643  nosupres  27644  nosupbnd1lem1  27645  nosupbnd1lem3  27647  nosupbnd1lem5  27649  nosupbnd2  27653  noinfcbv  27654  noinfno  27655  noinfdm  27656  noinffv  27658  noinfres  27659  noinfbnd1lem1  27660  noinfbnd1lem3  27662  noinfbnd1lem5  27664  noinfbnd2  27668  eulerpartlemt  34379  eulerpartlemgv  34381  eulerpartlemn  34389  eulerpart  34390  bnj1385  34839  bnj66  34867  bnj1234  35020  bnj1326  35033  bnj1463  35062  iscvm  35291  mbfresfi  37705  sdclem2  37781  isdivrngo  37989  evlselvlem  42618  evlselv  42619  mzpcompact2lem  42783  diophrw  42791  eldioph2lem1  42792  eldioph2lem2  42793  eldioph3  42798  diophin  42804  diophrex  42807  rexrabdioph  42826  2rexfrabdioph  42828  3rexfrabdioph  42829  4rexfrabdioph  42830  6rexfrabdioph  42831  7rexfrabdioph  42832  eldioph4b  42843  pwssplit4  43121  dvnprodlem1  45983  dvnprodlem3  45985  ismea  46488  isome  46531