Theorem reseq1 5874

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

Syntax hints:   → wi 4   = wceq 1539  Vcvv 3422   ∩ cin 3882   × cxp 5578   ↾ cres 5582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-in 3890  df-res 5592

This theorem is referenced by:  reseq1i  5876  reseq1d  5879  imaeq1  5953  fvtresfn  6859  frrlem1  8073  frrlem13  8085  wfrlem1OLD  8110  wfrlem3OLDa  8113  wfrlem15OLD  8125  tfrlem12  8191  pmresg  8616  resixpfo  8682  mapunen  8882  trpredlem1  9405  trpredtr  9408  trpredmintr  9409  fseqenlem1  9711  axdc3lem2  10138  axdc3lem4  10140  axdc  10208  hashf1lem1  14096  hashf1lem1OLD  14097  lo1eq  15205  rlimeq  15206  symgfixfo  18962  lspextmo  20233  evlseu  21203  mdetunilem3  21671  mdetunilem4  21672  mdetunilem9  21677  lmbr  22317  ptuncnv  22866  iscau  24345  plyexmo  25378  relogf1o  25627  eulerpartlemt  32238  eulerpartlemgv  32240  eulerpartlemn  32248  eulerpart  32249  bnj1385  32712  bnj66  32740  bnj1234  32893  bnj1326  32906  bnj1463  32935  iscvm  33121  nosupprefixmo  33830  noinfprefixmo  33831  nosupcbv  33832  nosupno  33833  nosupdm  33834  nosupfv  33836  nosupres  33837  nosupbnd1lem1  33838  nosupbnd1lem3  33840  nosupbnd1lem5  33842  nosupbnd2  33846  noinfcbv  33847  noinfno  33848  noinfdm  33849  noinffv  33851  noinfres  33852  noinfbnd1lem1  33853  noinfbnd1lem3  33855  noinfbnd1lem5  33857  noinfbnd2  33861  mbfresfi  35750  eqfnun  35807  sdclem2  35827  isdivrngo  36035  mzpcompact2lem  40489  diophrw  40497  eldioph2lem1  40498  eldioph2lem2  40499  eldioph3  40504  diophin  40510  diophrex  40513  rexrabdioph  40532  2rexfrabdioph  40534  3rexfrabdioph  40535  4rexfrabdioph  40536  6rexfrabdioph  40537  7rexfrabdioph  40538  eldioph4b  40549  pwssplit4  40830  dvnprodlem1  43377  dvnprodlem3  43379  ismea  43879  isome  43922