MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reseq2i Structured version   Visualization version   GIF version

Theorem reseq2i 5425
Description: Equality inference for restrictions. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypothesis
Ref Expression
reseqi.1 𝐴 = 𝐵
Assertion
Ref Expression
reseq2i (𝐶𝐴) = (𝐶𝐵)

Proof of Theorem reseq2i
StepHypRef Expression
1 reseqi.1 . 2 𝐴 = 𝐵
2 reseq2 5423 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2ax-mp 5 1 (𝐶𝐴) = (𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523  cres 5145
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-in 3614  df-opab 4746  df-xp 5149  df-res 5155
This theorem is referenced by:  reseq12i  5426  rescom  5458  resdmdfsn  5480  rescnvcnv  5632  resdm2  5662  funcnvres  6005  resasplit  6112  fresaunres2  6114  fresaunres1  6115  resdif  6195  resin  6196  funcocnv2  6199  fvn0ssdmfun  6390  residpr  6449  wfrlem5  7464  domss2  8160  ordtypelem1  8464  ackbij2lem3  9101  facnn  13102  fac0  13103  hashresfn  13168  relexpcnv  13819  divcnvshft  14631  ruclem4  15007  fsets  15938  setsid  15961  meet0  17184  join0  17185  symgfixelsi  17901  psgnsn  17986  dprd2da  18487  ply1plusgfvi  19660  uptx  21476  txcn  21477  ressxms  22377  ressms  22378  iscmet3lem3  23134  volres  23342  dvlip  23801  dvne0  23819  lhop  23824  dflog2  24352  dfrelog  24357  dvlog  24442  wilthlem2  24840  0grsubgr  26215  0pth  27103  1pthdlem1  27113  eupth2lemb  27215  df1stres  29609  df2ndres  29610  ffsrn  29632  resf1o  29633  fpwrelmapffs  29637  sitmcl  30541  eulerpartlemn  30571  bnj1326  31220  divcnvlin  31744  eqfunressuc  31786  frrlem5  31909  nosupbnd2lem1  31986  poimirlem9  33548  zrdivrng  33882  isdrngo1  33885  cnvresrn  34256  eldioph4b  37692  diophren  37694  rclexi  38239  rtrclex  38241  cnvrcl0  38249  dfrtrcl5  38253  dfrcl2  38283  relexpiidm  38313  relexp01min  38322  relexpaddss  38327  seff  38825  sblpnf  38826  radcnvrat  38830  hashnzfzclim  38838  dvresioo  40454  fourierdlem72  40713  fourierdlem80  40721  fourierdlem94  40735  fourierdlem103  40744  fourierdlem104  40745  fourierdlem113  40754  fouriersw  40766  sge0split  40944  rngcidALTV  42316  ringcidALTV  42379
  Copyright terms: Public domain W3C validator