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

Theorem reseq2i 5531
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 5529 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2ax-mp 5 1 (𝐶𝐴) = (𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1631  cres 5251
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-in 3730  df-opab 4847  df-xp 5255  df-res 5261
This theorem is referenced by:  reseq12i  5532  rescom  5564  resdmdfsn  5586  rescnvcnv  5738  resdm2  5768  funcnvres  6107  resasplit  6214  fresaunres2  6216  fresaunres1  6217  resdif  6298  resin  6299  funcocnv2  6302  fvn0ssdmfun  6493  residpr  6552  wfrlem5  7572  domss2  8275  ordtypelem1  8579  ackbij2lem3  9265  facnn  13266  fac0  13267  hashresfn  13332  relexpcnv  13983  divcnvshft  14794  ruclem4  15169  fsets  16098  setsid  16121  meet0  17345  join0  17346  symgfixelsi  18062  psgnsn  18147  dprd2da  18649  ply1plusgfvi  19827  uptx  21649  txcn  21650  ressxms  22550  ressms  22551  iscmet3lem3  23307  volres  23516  dvlip  23976  dvne0  23994  lhop  23999  dflog2  24528  dfrelog  24533  dvlog  24618  wilthlem2  25016  0grsubgr  26393  0pth  27305  1pthdlem1  27315  eupth2lemb  27417  clwwlknonclwlknonf1oOLD  27551  dlwwlknondlwlknonf1oOLD  27556  df1stres  29821  df2ndres  29822  ffsrn  29844  resf1o  29845  fpwrelmapffs  29849  sitmcl  30753  eulerpartlemn  30783  bnj1326  31432  divcnvlin  31956  eqfunressuc  31998  frrlem5  32121  nosupbnd2lem1  32198  poimirlem9  33751  zrdivrng  34084  isdrngo1  34087  cnvresrn  34458  eldioph4b  37901  diophren  37903  rclexi  38448  rtrclex  38450  cnvrcl0  38458  dfrtrcl5  38462  dfrcl2  38492  relexpiidm  38522  relexp01min  38531  relexpaddss  38536  seff  39034  sblpnf  39035  radcnvrat  39039  hashnzfzclim  39047  dvresioo  40654  fourierdlem72  40912  fourierdlem80  40920  fourierdlem94  40934  fourierdlem103  40943  fourierdlem104  40944  fourierdlem113  40953  fouriersw  40965  sge0split  41143  rngcidALTV  42519  ringcidALTV  42582
  Copyright terms: Public domain W3C validator