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

Theorem reseq2i 5594
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 5592 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2ax-mp 5 1 (𝐶𝐴) = (𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1637  cres 5313
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-v 3393  df-in 3776  df-opab 4907  df-xp 5317  df-res 5323
This theorem is referenced by:  reseq12i  5595  rescom  5626  resdmdfsn  5650  rescnvcnv  5808  resdm2  5838  funcnvres  6174  resasplit  6285  fresaunres2  6287  fresaunres1  6288  resdif  6369  resin  6370  funcocnv2  6373  fvn0ssdmfun  6568  residpr  6628  wfrlem5  7651  domss2  8354  ordtypelem1  8658  ackbij2lem3  9344  facnn  13278  fac0  13279  hashresfn  13344  relexpcnv  13994  divcnvshft  14805  ruclem4  15179  fsets  16098  setsid  16121  meet0  17338  join0  17339  symgfixelsi  18052  psgnsn  18137  dprd2da  18639  ply1plusgfvi  19816  uptx  21639  txcn  21640  ressxms  22540  ressms  22541  iscmet3lem3  23298  volres  23508  dvlip  23969  dvne0  23987  lhop  23992  dflog2  24520  dfrelog  24525  dvlog  24610  wilthlem2  25008  0grsubgr  26385  0pth  27297  1pthdlem1  27307  eupth2lemb  27409  df1stres  29807  df2ndres  29808  ffsrn  29830  resf1o  29831  fpwrelmapffs  29835  sitmcl  30737  eulerpartlemn  30767  bnj1326  31415  divcnvlin  31938  eqfunressuc  31980  frrlem5  32103  nosupbnd2lem1  32180  poimirlem9  33729  zrdivrng  34061  isdrngo1  34064  cnvresrn  34427  eldioph4b  37874  diophren  37876  rclexi  38419  rtrclex  38421  cnvrcl0  38429  dfrtrcl5  38433  dfrcl2  38463  relexpiidm  38493  relexp01min  38502  relexpaddss  38507  seff  39005  sblpnf  39006  radcnvrat  39010  hashnzfzclim  39018  dvresioo  40613  fourierdlem72  40871  fourierdlem80  40879  fourierdlem94  40893  fourierdlem103  40902  fourierdlem104  40903  fourierdlem113  40912  fouriersw  40924  sge0split  41102  rngcidALTV  42556  ringcidALTV  42619
  Copyright terms: Public domain W3C validator