Theorem reseq1 5390

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

Syntax hints:   → wi 4   = wceq 1483  Vcvv 3200   ∩ cin 3573   × cxp 5112   ↾ cres 5116

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-res 5126

This theorem is referenced by:  reseq1i  5392  reseq1d  5395  imaeq1  5461  fvtresfn  6284  wfrlem1  7414  wfrlem3a  7417  wfrlem15  7429  tfrlem12  7485  pmresg  7885  resixpfo  7946  mapunen  8129  fseqenlem1  8847  axdc3lem2  9273  axdc3lem4  9275  axdc  9343  hashf1lem1  13239  lo1eq  14299  rlimeq  14300  symgfixfo  17859  lspextmo  19056  evlseu  19516  mdetunilem3  20420  mdetunilem4  20421  mdetunilem9  20426  lmbr  21062  ptuncnv  21610  iscau  23074  plyexmo  24068  relogf1o  24313  eulerpartlemt  30433  eulerpartlemgv  30435  eulerpartlemn  30443  eulerpart  30444  bnj1385  30903  bnj66  30930  bnj1234  31081  bnj1326  31094  bnj1463  31123  iscvm  31241  trpredlem1  31727  trpredtr  31730  trpredmintr  31731  frrlem1  31780  noprefixmo  31848  nosupno  31849  nosupdm  31850  nosupfv  31852  nosupres  31853  nosupbnd1lem1  31854  nosupbnd1lem3  31856  nosupbnd1lem5  31858  nosupbnd2  31862  mbfresfi  33456  eqfnun  33516  sdclem2  33538  isdivrngo  33749  mzpcompact2lem  37314  diophrw  37322  eldioph2lem1  37323  eldioph2lem2  37324  eldioph3  37329  diophin  37336  diophrex  37339  rexrabdioph  37358  2rexfrabdioph  37360  3rexfrabdioph  37361  4rexfrabdioph  37362  6rexfrabdioph  37363  7rexfrabdioph  37364  eldioph4b  37375  pwssplit4  37659  dvnprodlem1  40161  dvnprodlem3  40163  ismea  40668  isome  40708