Theorem reseq1i 5975

Description: Equality inference for restrictions. (Contributed by NM, 21-Oct-2014.)

Hypothesis

Ref	Expression
reseqi.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
reseq1i	⊢ (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶)

Proof of Theorem reseq1i

Step	Hyp	Ref	Expression
1		reseqi.1	. 2 ⊢ 𝐴 = 𝐵
2		reseq1 5973	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶)

Syntax hints:   = wceq 1534   ↾ cres 5674

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3429  df-in 3952  df-res 5684

This theorem is referenced by:  reseq12i  5977  resindm  6028  resmpt  6035  resmpt3  6036  resmptf  6037  opabresid  6047  rescnvcnv  6202  coires1  6262  fnunres2  6661  fresaunres1  6764  fcoi1  6765  fninfp  7177  fvsnun1  7185  fvsnun2  7186  resoprab  7532  resmpo  7534  elimampo  7552  elrnmpores  7553  ofmres  7982  f1stres  8011  f2ndres  8012  df1st2  8097  df2nd2  8098  fsplitfpar  8117  dftpos2  8242  frrlem12  8296  wfrlem14OLD  8336  tfr2a  8409  tfr2b  8410  rdgseg  8436  frsucmpt2  8454  seqomlem2  8465  seqomlem3  8466  seqomlem4  8467  domss2  9154  dffi3  9448  fpwwe2lem12  10659  seqval  14003  hashgval  14318  hashinf  14320  submefmnd  18840  pgrpsubgsymg  19357  gsumzunsnd  19904  ablfac1b  20020  zzngim  21479  pmatcollpw3lem  22678  txflf  23903  xmsxmet2  24358  msmet2  24359  tmsxpsmopn  24439  isngp2  24499  subgnm  24535  tngngp2  24562  cnfldms  24685  msdcn  24750  oprpiece1res1  24869  oprpiece1res2  24870  isncvsngp  25070  cncms  25276  cnfldcusp  25278  reust  25302  minveclem3a  25348  dvreslem  25831  dvres2lem  25832  dvmptresicc  25838  dvcmulf  25869  mdegfval  25991  psercn  26356  abelth  26371  efcvx  26379  efifo  26474  dfrelog  26492  dvrelog  26564  dvlog  26578  efopnlem2  26584  dvatan  26860  dchrisumlem1  27415  noetasuplem2  27660  noetasuplem3  27661  noetasuplem4  27662  noetainflem2  27664  wlknwwlksnbij  29692  elimampt  32416  df1stres  32477  df2ndres  32478  padct  32495  ressplusf  32678  ressnm  32679  gsummpt2d  32757  cycpmrn  32858  tocyccntz  32859  cycpmconjslem2  32870  qusima  33112  qqhcn  33586  cnrrext  33605  rrhre  33616  esumcvg  33699  dya2icoseg2  33892  eulerpartgbij  33986  satf0  34976  neibastop2  35839  mptsnunlem  36811  icorempo  36824  poimirlem3  37090  mbfposadd  37134  ftc1anclem3  37162  dvasin  37171  dvacos  37172  prdsbnd2  37262  repwsmet  37301  rrnequiv  37302  inres2  37710  xrnres  37868  xrnres2  37869  xrnres3  37870  diophin  42186  eldioph4b  42225  dnnumch1  42462  aomclem6  42477  radcnvrat  43745  lhe4.4ex1a  43760  dvsid  43762  dvsef  43763  imassmpt  44633  elicores  44912  climresmpt  45041  dvcosre  45294  itgsinexplem1  45336  fourierdlem40  45529  fourierdlem57  45545  fourierdlem58  45546  fourierdlem62  45550  fourierdlem74  45562  fourierdlem75  45563  fourierdlem76  45564  fourierdlem80  45568  fourierdlem84  45572  fourierdlem85  45573  fourierdlem101  45589  fourierdlem102  45590  fourierdlem111  45599  fourierdlem114  45602  fouriersw  45613  fouriercn  45614  volicorescl  45935  fdmdifeqresdif  47399  aacllem  48228

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »