Theorem reseq1 5963

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

Syntax hints:   → wi 4   = wceq 1563  Vcvv 3457   ∩ cin 3906   × cxp 5650   ↾ cres 5654

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-in 3914  df-res 5664

This theorem is referenced by:  reseq1i  5965  reseq1d  5968  imaeq1  6048  fvtresfn  6982  eqfnun  7022  frrlem1  8271  frrlem13  8283  tfrlem12  8364  pmresg  8856  resixpfo  8922  mapunen  9122  fseqenlem1  9996  axdc3lem2  10423  axdc3lem4  10425  hashf1lem1  14482  lo1eq  15609  rlimeq  15610  symgfixfo  19500  lspextmo  21146  evlseu  22194  mdetunilem3  22732  mdetunilem4  22733  mdetunilem9  22738  lmbr  23376  ptuncnv  23925  iscau  25396  plyexmo  26435  relogf1o  26689  nosupprefixmo  27822  noinfprefixmo  27823  nosupcbv  27824  nosupno  27825  nosupdm  27826  nosupfv  27828  nosupres  27829  nosupbnd1lem1  27830  nosupbnd1lem3  27832  nosupbnd1lem5  27834  nosupbnd2  27838  noinfcbv  27839  noinfno  27840  noinfdm  27841  noinffv  27843  noinfres  27844  noinfbnd1lem1  27845  noinfbnd1lem3  27847  noinfbnd1lem5  27849  noinfbnd2  27853  extvfvv  33841  extvfvcl  33843  eulerpartlemt  34678  eulerpartlemgv  34680  eulerpartlemn  34688  eulerpart  34689  bnj1385  35137  bnj66  35165  bnj1234  35318  bnj1326  35331  bnj1463  35360  iscvm  35622  mbfresfi  38177  sdclem2  38253  isdivrngo  38461  evlselvlem  43182  evlselv  43183  mzpcompact2lem  43344  diophrw  43352  eldioph2lem1  43353  eldioph2lem2  43354  eldioph3  43359  diophin  43365  diophrex  43368  rexrabdioph  43383  2rexfrabdioph  43385  3rexfrabdioph  43386  4rexfrabdioph  43387  6rexfrabdioph  43388  7rexfrabdioph  43389  eldioph4b  43400  pwssplit4  43678  dvnprodlem1  46518  dvnprodlem3  46520  ismea  47023  isome  47066