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

Theorem reseq2i 5353
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 5351 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2ax-mp 5 1 (𝐶𝐴) = (𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  cres 5076
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3188  df-in 3562  df-opab 4674  df-xp 5080  df-res 5086
This theorem is referenced by:  reseq12i  5354  rescom  5382  resdmdfsn  5404  rescnvcnv  5556  resdm2  5583  funcnvres  5925  resasplit  6031  fresaunres2  6033  fresaunres1  6034  resdif  6114  resin  6115  funcocnv2  6118  fvn0ssdmfun  6306  residpr  6363  wfrlem5  7364  domss2  8063  ordtypelem1  8367  ackbij2lem3  9007  facnn  13002  fac0  13003  hashresfn  13068  relexpcnv  13709  divcnvshft  14512  ruclem4  14888  fsets  15812  setsid  15835  meet0  17058  join0  17059  symgfixelsi  17776  psgnsn  17861  dprd2da  18362  ply1plusgfvi  19531  uptx  21338  txcn  21339  ressxms  22240  ressms  22241  iscmet3lem3  22996  volres  23203  dvlip  23660  dvne0  23678  lhop  23683  dflog2  24211  dfrelog  24216  dvlog  24297  wilthlem2  24695  0grsubgr  26063  0pth  26852  1pthdlem1  26861  eupth2lemb  26963  df1stres  29324  df2ndres  29325  ffsrn  29347  resf1o  29348  fpwrelmapffs  29352  sitmcl  30194  eulerpartlemn  30224  bnj1326  30802  divcnvlin  31326  frrlem5  31485  poimirlem9  33050  zrdivrng  33384  isdrngo1  33387  eldioph4b  36855  diophren  36857  rclexi  37403  rtrclex  37405  cnvrcl0  37413  dfrtrcl5  37417  dfrcl2  37447  relexpiidm  37477  relexp01min  37486  relexpaddss  37491  seff  37990  sblpnf  37991  radcnvrat  37995  hashnzfzclim  38003  dvresioo  39442  fourierdlem72  39702  fourierdlem80  39710  fourierdlem94  39724  fourierdlem103  39733  fourierdlem104  39734  fourierdlem113  39743  fouriersw  39755  sge0split  39933  rngcidALTV  41279  ringcidALTV  41342
  Copyright terms: Public domain W3C validator