Theorem reseq1 5932

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

Syntax hints:   → wi 4   = wceq 1547  Vcvv 3432   ∩ cin 3889   × cxp 5623   ↾ cres 5627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-in 3897  df-res 5637

This theorem is referenced by:  reseq1i  5934  reseq1d  5937  imaeq1  6014  fvtresfn  6945  eqfnun  6985  frrlem1  8233  frrlem13  8245  tfrlem12  8325  pmresg  8815  resixpfo  8881  mapunen  9081  fseqenlem1  9944  axdc3lem2  10371  axdc3lem4  10373  hashf1lem1  14415  lo1eq  15528  rlimeq  15529  symgfixfo  19412  lspextmo  21053  evlseu  22066  mdetunilem3  22604  mdetunilem4  22605  mdetunilem9  22610  lmbr  23248  ptuncnv  23797  iscau  25268  plyexmo  26304  relogf1o  26555  nosupprefixmo  27689  noinfprefixmo  27690  nosupcbv  27691  nosupno  27692  nosupdm  27693  nosupfv  27695  nosupres  27696  nosupbnd1lem1  27697  nosupbnd1lem3  27699  nosupbnd1lem5  27701  nosupbnd2  27705  noinfcbv  27706  noinfno  27707  noinfdm  27708  noinffv  27710  noinfres  27711  noinfbnd1lem1  27712  noinfbnd1lem3  27714  noinfbnd1lem5  27716  noinfbnd2  27720  extvfvv  33725  extvfvcl  33727  eulerpartlemt  34562  eulerpartlemgv  34564  eulerpartlemn  34572  eulerpart  34573  bnj1385  35021  bnj66  35049  bnj1234  35202  bnj1326  35215  bnj1463  35244  iscvm  35494  mbfresfi  38040  sdclem2  38116  isdivrngo  38324  evlselvlem  43045  evlselv  43046  mzpcompact2lem  43207  diophrw  43215  eldioph2lem1  43216  eldioph2lem2  43217  eldioph3  43222  diophin  43228  diophrex  43231  rexrabdioph  43246  2rexfrabdioph  43248  3rexfrabdioph  43249  4rexfrabdioph  43250  6rexfrabdioph  43251  7rexfrabdioph  43252  eldioph4b  43263  pwssplit4  43541  dvnprodlem1  46396  dvnprodlem3  46398  ismea  46901  isome  46944