Theorem reseq1 5944

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

Syntax hints:   → wi 4   = wceq 1540  Vcvv 3447   ∩ cin 3913   × cxp 5636   ↾ cres 5640

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-in 3921  df-res 5650

This theorem is referenced by:  reseq1i  5946  reseq1d  5949  imaeq1  6026  fvtresfn  6970  eqfnun  7009  frrlem1  8265  frrlem13  8277  tfrlem12  8357  pmresg  8843  resixpfo  8909  mapunen  9110  fseqenlem1  9977  axdc3lem2  10404  axdc3lem4  10406  hashf1lem1  14420  lo1eq  15534  rlimeq  15535  symgfixfo  19369  lspextmo  20963  evlseu  21990  mdetunilem3  22501  mdetunilem4  22502  mdetunilem9  22507  lmbr  23145  ptuncnv  23694  iscau  25176  plyexmo  26221  relogf1o  26475  nosupprefixmo  27612  noinfprefixmo  27613  nosupcbv  27614  nosupno  27615  nosupdm  27616  nosupfv  27618  nosupres  27619  nosupbnd1lem1  27620  nosupbnd1lem3  27622  nosupbnd1lem5  27624  nosupbnd2  27628  noinfcbv  27629  noinfno  27630  noinfdm  27631  noinffv  27633  noinfres  27634  noinfbnd1lem1  27635  noinfbnd1lem3  27637  noinfbnd1lem5  27639  noinfbnd2  27643  eulerpartlemt  34362  eulerpartlemgv  34364  eulerpartlemn  34372  eulerpart  34373  bnj1385  34822  bnj66  34850  bnj1234  35003  bnj1326  35016  bnj1463  35045  iscvm  35246  mbfresfi  37660  sdclem2  37736  isdivrngo  37944  evlselvlem  42574  evlselv  42575  mzpcompact2lem  42739  diophrw  42747  eldioph2lem1  42748  eldioph2lem2  42749  eldioph3  42754  diophin  42760  diophrex  42763  rexrabdioph  42782  2rexfrabdioph  42784  3rexfrabdioph  42785  4rexfrabdioph  42786  6rexfrabdioph  42787  7rexfrabdioph  42788  eldioph4b  42799  pwssplit4  43078  dvnprodlem1  45944  dvnprodlem3  45946  ismea  46449  isome  46492