Theorem reseq1 5991

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

Syntax hints:   → wi 4   = wceq 1540  Vcvv 3480   ∩ cin 3950   × cxp 5683   ↾ cres 5687

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-in 3958  df-res 5697

This theorem is referenced by:  reseq1i  5993  reseq1d  5996  imaeq1  6073  fvtresfn  7018  eqfnun  7057  frrlem1  8311  frrlem13  8323  wfrlem1OLD  8348  wfrlem3OLDa  8351  wfrlem15OLD  8363  tfrlem12  8429  pmresg  8910  resixpfo  8976  mapunen  9186  fseqenlem1  10064  axdc3lem2  10491  axdc3lem4  10493  hashf1lem1  14494  lo1eq  15604  rlimeq  15605  symgfixfo  19457  lspextmo  21055  evlseu  22107  mdetunilem3  22620  mdetunilem4  22621  mdetunilem9  22626  lmbr  23266  ptuncnv  23815  iscau  25310  plyexmo  26355  relogf1o  26608  nosupprefixmo  27745  noinfprefixmo  27746  nosupcbv  27747  nosupno  27748  nosupdm  27749  nosupfv  27751  nosupres  27752  nosupbnd1lem1  27753  nosupbnd1lem3  27755  nosupbnd1lem5  27757  nosupbnd2  27761  noinfcbv  27762  noinfno  27763  noinfdm  27764  noinffv  27766  noinfres  27767  noinfbnd1lem1  27768  noinfbnd1lem3  27770  noinfbnd1lem5  27772  noinfbnd2  27776  eulerpartlemt  34373  eulerpartlemgv  34375  eulerpartlemn  34383  eulerpart  34384  bnj1385  34846  bnj66  34874  bnj1234  35027  bnj1326  35040  bnj1463  35069  iscvm  35264  mbfresfi  37673  sdclem2  37749  isdivrngo  37957  evlselvlem  42596  evlselv  42597  mzpcompact2lem  42762  diophrw  42770  eldioph2lem1  42771  eldioph2lem2  42772  eldioph3  42777  diophin  42783  diophrex  42786  rexrabdioph  42805  2rexfrabdioph  42807  3rexfrabdioph  42808  4rexfrabdioph  42809  6rexfrabdioph  42810  7rexfrabdioph  42811  eldioph4b  42822  pwssplit4  43101  dvnprodlem1  45961  dvnprodlem3  45963  ismea  46466  isome  46509