Theorem reseq1 5977

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  Vcvv 3458   ∩ cin 3907   × cxp 5664   ↾ cres 5668

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-in 3915  df-res 5678

This theorem is used by:  reseq1i  5979  reseq1d  5982  imaeq1  6062  fvtresfn  6999  eqfnun  7039  frrlem1  8292  frrlem13  8304  tfrlem12  8385  pmresg  8877  resixpfo  8943  mapunen  9144  fseqenlem1  10027  axdc3lem2  10453  axdc3lem4  10455  hashf1lem1  14512  lo1eq  15645  rlimeq  15646  symgfixfo  19540  lspextmo  21214  evlseu  22271  mdetunilem3  22808  mdetunilem4  22809  mdetunilem9  22814  lmbr  23452  ptuncnv  24001  iscau  25472  plyexmo  26511  relogf1o  26768  nosupprefixmo  27901  noinfprefixmo  27902  nosupcbv  27903  nosupno  27904  nosupdm  27905  nosupfv  27907  nosupres  27908  nosupbnd1lem1  27909  nosupbnd1lem3  27911  nosupbnd1lem5  27913  nosupbnd2  27917  noinfcbv  27918  noinfno  27919  noinfdm  27920  noinffv  27922  noinfres  27923  noinfbnd1lem1  27924  noinfbnd1lem3  27926  noinfbnd1lem5  27928  noinfbnd2  27932  extvfvv  33955  extvfvcl  33957  eulerpartlemt  34793  eulerpartlemgv  34795  eulerpartlemn  34803  eulerpart  34804  bnj1385  35252  bnj66  35280  bnj1234  35433  bnj1326  35446  bnj1463  35475  iscvm  35772  mbfresfi  38358  sdclem2  38434  isdivrngo  38642  evlselvlem  43361  evlselv  43362  mzpcompact2lem  43523  diophrw  43531  eldioph2lem1  43532  eldioph2lem2  43533  eldioph3  43538  diophin  43544  diophrex  43547  rexrabdioph  43562  2rexfrabdioph  43564  3rexfrabdioph  43565  4rexfrabdioph  43566  6rexfrabdioph  43567  7rexfrabdioph  43568  eldioph4b  43579  pwssplit4  43857  dvnprodlem1  46701  dvnprodlem3  46703  ismea  47206  isome  47249