Theorem reseq1 5638

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

Syntax hints:   → wi 4   = wceq 1601  Vcvv 3398   ∩ cin 3791   × cxp 5355   ↾ cres 5359

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-v 3400  df-in 3799  df-res 5369

This theorem is referenced by:  reseq1i  5640  reseq1d  5643  imaeq1  5717  fvtresfn  6546  wfrlem1  7698  wfrlem3a  7701  wfrlem15  7714  tfrlem12  7770  pmresg  8170  resixpfo  8234  mapunen  8419  fseqenlem1  9182  axdc3lem2  9610  axdc3lem4  9612  axdc  9680  hashf1lem1  13557  lo1eq  14711  rlimeq  14712  symgfixfo  18246  lspextmo  19455  evlseu  19916  mdetunilem3  20829  mdetunilem4  20830  mdetunilem9  20835  lmbr  21474  ptuncnv  22023  iscau  23486  plyexmo  24509  relogf1o  24754  eulerpartlemt  31035  eulerpartlemgv  31037  eulerpartlemn  31045  eulerpart  31046  bnj1385  31506  bnj66  31533  bnj1234  31684  bnj1326  31697  bnj1463  31726  iscvm  31844  trpredlem1  32319  trpredtr  32322  trpredmintr  32323  frrlem1  32373  noprefixmo  32441  nosupno  32442  nosupdm  32443  nosupfv  32445  nosupres  32446  nosupbnd1lem1  32447  nosupbnd1lem3  32449  nosupbnd1lem5  32451  nosupbnd2  32455  mbfresfi  34086  eqfnun  34146  sdclem2  34167  isdivrngo  34378  mzpcompact2lem  38284  diophrw  38292  eldioph2lem1  38293  eldioph2lem2  38294  eldioph3  38299  diophin  38306  diophrex  38309  rexrabdioph  38328  2rexfrabdioph  38330  3rexfrabdioph  38331  4rexfrabdioph  38332  6rexfrabdioph  38333  7rexfrabdioph  38334  eldioph4b  38345  pwssplit4  38628  dvnprodlem1  41099  dvnprodlem3  41101  ismea  41602  isome  41645