Theorem reseq1 5976

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

Syntax hints:   → wi 4   = wceq 1542  Vcvv 3475   ∩ cin 3948   × cxp 5675   ↾ cres 5679

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-in 3956  df-res 5689

This theorem is referenced by:  reseq1i  5978  reseq1d  5981  imaeq1  6055  fvtresfn  7001  eqfnun  7039  frrlem1  8271  frrlem13  8283  wfrlem1OLD  8308  wfrlem3OLDa  8311  wfrlem15OLD  8323  tfrlem12  8389  pmresg  8864  resixpfo  8930  mapunen  9146  fseqenlem1  10019  axdc3lem2  10446  axdc3lem4  10448  axdc  10516  hashf1lem1  14415  hashf1lem1OLD  14416  lo1eq  15512  rlimeq  15513  symgfixfo  19307  lspextmo  20667  evlseu  21646  mdetunilem3  22116  mdetunilem4  22117  mdetunilem9  22122  lmbr  22762  ptuncnv  23311  iscau  24793  plyexmo  25826  relogf1o  26075  nosupprefixmo  27203  noinfprefixmo  27204  nosupcbv  27205  nosupno  27206  nosupdm  27207  nosupfv  27209  nosupres  27210  nosupbnd1lem1  27211  nosupbnd1lem3  27213  nosupbnd1lem5  27215  nosupbnd2  27219  noinfcbv  27220  noinfno  27221  noinfdm  27222  noinffv  27224  noinfres  27225  noinfbnd1lem1  27226  noinfbnd1lem3  27228  noinfbnd1lem5  27230  noinfbnd2  27234  eulerpartlemt  33401  eulerpartlemgv  33403  eulerpartlemn  33411  eulerpart  33412  bnj1385  33874  bnj66  33902  bnj1234  34055  bnj1326  34068  bnj1463  34097  iscvm  34281  mbfresfi  36582  sdclem2  36658  isdivrngo  36866  evlselvlem  41206  evlselv  41207  mzpcompact2lem  41537  diophrw  41545  eldioph2lem1  41546  eldioph2lem2  41547  eldioph3  41552  diophin  41558  diophrex  41561  rexrabdioph  41580  2rexfrabdioph  41582  3rexfrabdioph  41583  4rexfrabdioph  41584  6rexfrabdioph  41585  7rexfrabdioph  41586  eldioph4b  41597  pwssplit4  41879  dvnprodlem1  44710  dvnprodlem3  44712  ismea  45215  isome  45258