Theorem reseq1 5957

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

Syntax hints:   → wi 4   = wceq 1559  Vcvv 3453   ∩ cin 3903   × cxp 5643   ↾ cres 5647

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-in 3911  df-res 5657

This theorem is referenced by:  reseq1i  5959  reseq1d  5962  imaeq1  6041  fvtresfn  6974  eqfnun  7014  frrlem1  8262  frrlem13  8274  tfrlem12  8355  pmresg  8848  resixpfo  8914  mapunen  9114  fseqenlem1  9977  axdc3lem2  10405  axdc3lem4  10407  hashf1lem1  14465  lo1eq  15578  rlimeq  15579  symgfixfo  19462  lspextmo  21103  evlseu  22116  mdetunilem3  22654  mdetunilem4  22655  mdetunilem9  22660  lmbr  23298  ptuncnv  23847  iscau  25318  plyexmo  26354  relogf1o  26608  nosupprefixmo  27741  noinfprefixmo  27742  nosupcbv  27743  nosupno  27744  nosupdm  27745  nosupfv  27747  nosupres  27748  nosupbnd1lem1  27749  nosupbnd1lem3  27751  nosupbnd1lem5  27753  nosupbnd2  27757  noinfcbv  27758  noinfno  27759  noinfdm  27760  noinffv  27762  noinfres  27763  noinfbnd1lem1  27764  noinfbnd1lem3  27766  noinfbnd1lem5  27768  noinfbnd2  27772  extvfvv  33792  extvfvcl  33794  eulerpartlemt  34629  eulerpartlemgv  34631  eulerpartlemn  34639  eulerpart  34640  bnj1385  35091  bnj66  35119  bnj1234  35272  bnj1326  35285  bnj1463  35314  iscvm  35573  mbfresfi  38129  sdclem2  38205  isdivrngo  38413  evlselvlem  43134  evlselv  43135  mzpcompact2lem  43296  diophrw  43304  eldioph2lem1  43305  eldioph2lem2  43306  eldioph3  43311  diophin  43317  diophrex  43320  rexrabdioph  43335  2rexfrabdioph  43337  3rexfrabdioph  43338  4rexfrabdioph  43339  6rexfrabdioph  43340  7rexfrabdioph  43341  eldioph4b  43352  pwssplit4  43630  dvnprodlem1  46484  dvnprodlem3  46486  ismea  46989  isome  47032