Theorem reseq1 5976

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  Vcvv 3454   ∩ cin 4092   × cxp 5654   ↾ cres 5658

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-in 4094  df-res 5668

This theorem is used by:  reseq1i  5978  reseq1d  5981  imaeq1  6060  fvtresfn  7022  eqfnun  7062  frrlem1  8335  frrlem13  8347  tfrlem12  8428  pmresg  8929  resixpfo  8995  mapunen  9196  fseqenlem1  10133  axdc3lem2  10559  axdc3lem4  10561  hashf1lem1  14630  lo1eq  15767  rlimeq  15768  symgfixfo  19686  lspextmo  21364  evlseu  22425  mdetunilem3  22962  mdetunilem4  22963  mdetunilem9  22968  lmbr  23609  ptuncnv  24159  iscau  25630  plyexmo  26669  relogf1o  26927  nosupprefixmo  28090  noinfprefixmo  28091  nosupcbv  28092  nosupno  28093  nosupdm  28094  nosupfv  28096  nosupres  28097  nosupbnd1lem1  28098  nosupbnd1lem3  28100  nosupbnd1lem5  28102  nosupbnd2  28106  noinfcbv  28107  noinfno  28108  noinfdm  28109  noinffv  28111  noinfres  28112  noinfbnd1lem1  28113  noinfbnd1lem3  28115  noinfbnd1lem5  28117  noinfbnd2  28121  extvfvv  34249  extvfvcl  34251  eulerpartlemt  35086  eulerpartlemgv  35088  eulerpartlemn  35096  eulerpart  35097  bnj1385  35545  bnj66  35573  bnj1234  35726  bnj1326  35739  bnj1463  35768  gdlop4fv  35979  iscvm  36204  mbfresfi  38789  sdclem2  38879  isdivrngo  39087  evlselvlem  43820  evlselv  43821  mzpcompact2lem  43966  diophrw  43974  eldioph2lem1  43975  eldioph2lem2  43976  eldioph3  43981  diophin  43987  diophrex  43990  rexrabdioph  44005  2rexfrabdioph  44007  3rexfrabdioph  44008  4rexfrabdioph  44009  6rexfrabdioph  44010  7rexfrabdioph  44011  eldioph4b  44022  pwssplit4  44295  dvnprodlem1  47171  dvnprodlem3  47173  ismea  47676  isome  47719  tmachlem-agreeself  48161